Re: [isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

2018-01-14 Thread Gerwin.Klein 
Good points. I’ve added the slow/very_slow and x64 hints to the documentation 
now.

Cheers,
Gerwin

> On 15.01.2018, at 07:38, Makarius  wrote:
> 
> On 14/01/18 12:42, Clemens Ballarin wrote:
>> Dear Maintainers of Isabelle / the AFP,
>> 
>> Where would I find instructions on actually getting 'isabelle afp_build
>> -A' to run through?  I was hoping to find that in
>> /doc/regression-test.md but that merely states the command.
> 
> My command-line usually looks like this:
> 
>  isabelle build -d '$AFP' -a -X slow -j4
> 
> Or:
> 
>  isabelle build -d '$AFP' -a -X very_slow -j4
> 
> You can also use -D '$AFP' (without -a) to address precisely the AFP
> sessions.
> 
> 
>> It appears that I would need to set ML_PLATFORM=x86_64-darwin for the
>> large sessions but then some magic seems to defeat that and builds are
>> still for x86-darwin.
> 
> Instead of editing $ISABELLE_HOME_USER/etc/settings to change
> ML_PLATFORM (which is difficult to get right), I usually edit
> $ISABELLE_HOME_USER/etc/preferences to add:
> 
>  ML_system_64 = true
> 
> Only some "slow" sessions do need x86_64, but some non-slow sessions
> (like HOL-ODE-Numerics) become a bit slow in x86 mode. Almost everything
> else works better in x86 mode, which is the default.
> 
> See also
> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html
> for typical maximum heap requirements.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments for inner syntax etc.

2018-01-14 Thread Makarius 
On 11/01/18 14:51, Makarius wrote:
> 
> Isabelle/7360fe6bb423 is an example for a change to "prefer formal
> comments": this requires delicate work by hand, because the intended
> meaning of a comment can vary:
> 
>   (1) comment as plain text (with regular typesetting in the document)
>   (2) comment containing formal text, e.g. @{term} or @{cartouche}
>   (3) old/unwanted source text that is actually "commented-out"
> 
> I am in the process the update cases (1) and (2) in all of Isabelle +
> AFP, but case (3) is still untouched. The latter might require a
> different formal notation, e.g. \<^blank>\text\.

In the meantime I have manually updated Isabelle + AFP, using notation
\<^cancel>\text\ (with fancy rendering in
Isabelle/0b691782d6e5). The document output uses a version of
"strike-through" in LaTeX, e.g. see
https://devel.isa-afp.org/browser_info/current/AFP/SPARCv8/document.pdf
page 6 (definition of "get_S").

A bit more is emerging: uniform formal comments in outer and inner
syntax: \, \<^cancel>, \<^latex> (for raw LaTeX source). When
that is done, I will post a proper NEWS announcement.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

2018-01-14 Thread Makarius 
On 14/01/18 12:42, Clemens Ballarin wrote:
> Dear Maintainers of Isabelle / the AFP,
> 
> Where would I find instructions on actually getting 'isabelle afp_build
> -A' to run through?  I was hoping to find that in
> /doc/regression-test.md but that merely states the command.

My command-line usually looks like this:

  isabelle build -d '$AFP' -a -X slow -j4

Or:

  isabelle build -d '$AFP' -a -X very_slow -j4

You can also use -D '$AFP' (without -a) to address precisely the AFP
sessions.


> It appears that I would need to set ML_PLATFORM=x86_64-darwin for the
> large sessions but then some magic seems to defeat that and builds are
> still for x86-darwin.

Instead of editing $ISABELLE_HOME_USER/etc/settings to change
ML_PLATFORM (which is difficult to get right), I usually edit
$ISABELLE_HOME_USER/etc/preferences to add:

  ML_system_64 = true

Only some "slow" sessions do need x86_64, but some non-slow sessions
(like HOL-ODE-Numerics) become a bit slow in x86 mode. Almost everything
else works better in x86 mode, which is the default.

See also
http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html
for typical maximum heap requirements.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

2018-01-14 Thread Clemens Ballarin 

Dear Maintainers of Isabelle / the AFP,

Where would I find instructions on actually getting 'isabelle afp_build 
-A' to run through?  I was hoping to find that in 
/doc/regression-test.md but that merely states the command.


It appears that I would need to set ML_PLATFORM=x86_64-darwin for the 
large sessions but then some magic seems to defeat that and builds are 
still for x86-darwin.


Clemens
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev