[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"
lars at hupel.info
Wed Dec 23 10:08:48 CET 2020
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.
The first failing build log is:
Based on my superficial understanding, this problem appears to be caused
by two different theories including the same ML file
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.
More information about the isabelle-dev