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

Lars Hupel lars at hupel.info
Wed Dec 23 10:08:48 CET 2020

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. 

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.

Happy holidays,

More information about the isabelle-dev mailing list