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

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)

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

[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