Re: [isabelle] Isabelle2013-RC2 available for testing



Hi Makarius,

After experimenting with Isabelle2013-RC2 for Windows (in my W7 laptop), I
can give the following feedback:

1) Intialization of Cygwin this time was successfull. Avast did not find
any problem with the following
program:

C:\Isabelle2013-RC1\contrib\cygwin\bin\peflags.exe

2) Avast it is however still very suspicious (considering them of low
reputation) with these ones, allowing
them to execute in sandbox mode though (after scrutinizing each file for
about half a minute):

C:\Isabelle2013-RC1\Isabelle2013.exe
C:\Users\AlfioMartini\Isabelle2013-RC2\contrib\polyml-5.5.0-3\x86-cygwin\poly.exe
C:\Users\AlfioMartini\Isabelle2013-RC2\contrib\exec_process-1.0.3\x86-cygwin\exec_process.exe

3) Old style of processing documents (via IsaMakefiles) is now working
again in this version (see image
attached)

4) Executing

 isabelle build -o document=pdf -g doc

still shows the error when compiling the "Programming and Proving"
tutorial. Maybe the LaTeX setup
should be updated to include the package "eulervm.sty" or, as you suggest
in a previous e-mail,
that this package should not be used (or something else be used in its
place). See image attached.

5) Most important, those ambiguous and strange error messages (as discussed
in another live
thread) in the output window are
still present. I include here a file "error_test.thy" so you can see
exacty, on the spot, what
it is going on.

Best!

On Mon, Jan 28, 2013 at 3:01 PM, Makarius <makarius at sketis.net> wrote:

> Dear all,
>
> this is one more step towards the Isabelle2013 release in mid-February.
>
> See https://bitbucket.org/**isabelle_project/isabelle-**release<https://bitbucket.org/isabelle_project/isabelle-release>for the main website where this is organized.  There is also a link to an
> issue tracker on the same Bitbucket site.
>
> The main Isabelle2013-RC2 download page is http://isabelle.in.tum.de/**
> website-Isabelle2013-RC2<http://isabelle.in.tum.de/website-Isabelle2013-RC2>
>
> Observations from testing release candidates may be discussed here on
> isabelle-users, on the bitbucket tracker, or via private mail.
>
>
>         Makarius
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: RC2-docprep-old-way-sucess.PNG
Description: PNG image

Attachment: prog-prove-error.PNG
Description: PNG image

Attachment: error_test.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.