Hi Lars,
even without the slow sessions, this is of great help. Thanks!
My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because
without the afp_testboard, I used to follow the "break it, fix it” philosophy
w.r.t. AFP). I will repair those today.
Dmitriy
> On 17 Feb 2016,
> With such a painfully slow and incomplete SML/NJ test, it is time to ask
> the canonical question:
>
> Are there remaining uses of SML/NJ, or can it be discontinued now?
I would also prefer a second usable ML implementation as reference, but
we have to face that only maintained platforms as
Despite increasing the ML heap size with "-H 2000", the session
"Formula_Derivatives" is failing. The build VMs have 32 GB of RAM, so
that shouldn't be a problem. Here are the relevant environment variables:
ML_PLATFORM="x86-linux"
*** Isar ***
* Command '\' is an alias for 'sorry', with different
typesetting. E.g. to produce proof holes in examples and documentation.
This refers to Isabelle/5e5a881ebc12.
It means that manuals, tutorials, slides etc. may be written more easily,
without odd conditionals in LaTeX for the
