Stream: Mirror: Isabelle Development Mailing List

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


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC