Email Gateway (Dec 23 2020 at 13:22): Email Gateway (Dec 23 2020 at 13:22):From: Lars Hupel <lars@hupel.info>
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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Dec 23 2020 at 14:56):From: Makarius <makarius@sketis.net>
On 23/12/2020 10:08, Lars Hupel wrote:
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).
There is something conceptually wrong here. I will see how to get it right.
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.
Duplication is even worse.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Dec 23 2020 at 23:11):From: Makarius <makarius@sketis.net>
I have reworked it in Isabelle/b1be35908165, to make it fit better into
contemporary Isabelle.
Moreover, I have brushed up the HOL-Hoare session document in
Isabelle/db8f94656024.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Dec 29 2020 at 17:29):From: Lars Hupel <lars@hupel.info>
This fixed it for Hoare, but we have another problem:
10:01:16 *** Incoherent use of file name
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" as
"files/ISABELLE_HOME/src/Doc/antiquote_setup.ML.html" in theory
Isabelle_Meta_Model.Generator_static vs. Isabelle_Meta_Model.Design_deep
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 01 2021 at 09:24):From: Makarius <makarius@sketis.net>
I've returned from Christmas vacation yesterday and now see that you have
addressed it already in AFP/459344fb0c40.
The approach looks right: a theory context manages shared resources according
to the import graph structure.
At a later stage, I should probably merge ideas from
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" back into more official
antiquotations in Isabelle/Pure.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 01 2021 at 19:09):From: Lars Hupel <lars@hupel.info>
The approach looks right: a theory context manages shared resources according
to the import graph structure.
Sadly we now have a "total existence failure", as evidenced in
<https://ci.isabelle.systems/jenkins/job/isabelle-all/2573/consoleFull>
It appears that the JVM process just hangs when (or after) building the
document for the Network_Security_Policy_Verification session.
(Logfiles and Session DBs are available for download:
<https://ci.isabelle.systems/jenkins/job/isabelle-all/2573/artifact/heaps/polyml-5.8.2_x86_64_32-linux/log/>)
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 01 2021 at 23:12):From: Makarius <makarius@sketis.net>
I have stared at "consoleFull" a few minutes without spotting anything suspicious.
In Isabelle/38528017e4c8 there is some more verbosity, to see where it gets
stuck --- if it is repeatable at all.
Note that I did manage to build Isabelle + AFP with pdf + HTML several times
on other big machines, using settings like this:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms1g -Xmx8g -Xss16m"
ML_PLATFORM="x86_64_32-linux"
ML_OPTIONS="--minheap 1500"
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 02 2021 at 11:07):From: Makarius <makarius@sketis.net>
I have managed to reproduce the problem locally, and will come back with a
suitable change soon.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 02 2021 at 11:17):From: Lars Hupel <lars@hupel.info>
In Isabelle/38528017e4c8 there is some more verbosity, to see where it gets
stuck --- if it is repeatable at all.
It still gets stuck.
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 02 2021 at 23:51):From: Makarius <makarius@sketis.net>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 30 2024 at 12:36 UTC