Dear list,
since Isabelle/af2d0e07493b, presenting the HOL-Hoare session fails:
*** Incoherent use of file name "hoare_syntax.ML" as
"files/hoare_syntax.ML.html" in theory HOL-Hoare.Hoare_Logic vs.
HOL-Hoare.Hoare_Logic_Abort
The first failing build log is:
<https://ci.isabelle.systems/jenkins/job/isabelle-all/2543/consoleFull>
Based on my superficial understanding, this problem appears to be caused
by two different theories including the same ML file
(src/HOL/Hoare/hoare_syntax.ML).
Since the ML file is dependent on syntax that is independently
introduced by those theories, I'm unsure how to fix this. The naive
solution would be to duplicate the ML file, but that seems inelegant.
Happy holidays,
Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
