[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

Makarius makarius at sketis.net
Sun Jan 3 00:50:52 CET 2021


On 02/01/2021 12:07, Makarius wrote:
> On 02/01/2021 10:03, Lars Hupel wrote:
>>> In Isabelle/38528017e4c8 there is some more verbosity, to see where it gets
>>> stuck --- if it is repeatable at all.
>>
>> It still gets stuck.
> 
> I have managed to reproduce the problem locally, and will come back with a
> suitable change soon.

In Isabelle/43c534bba442 + AFP/a31f698ef3f8 everything should work.

HTML presentation is now much faster and more scalable, but it still takes
20min for all of AFP.


	Makarius



More information about the isabelle-dev mailing list