Email Gateway (Sep 26 2023 at 20:49): Email Gateway (Sep 26 2023 at 20:49):From: Peter Lammich <lammich@in.tum.de>
Hello List,
with Isabelle2023, I get odd errors when trying to build and present
theories depending on AFP entries (example attached).
I'm using afp-2023-09-26. With isabelle2023-RC5 and afp-devel
4605c928f00e everything worked fine, so I didn't report that earlier.
What is happening here? Is this caused by errors in the AFP entries, or
am I importing them the wrong way?
Currently, the only workaround to at least get isabelle jedit to start
with an image is to disable browser_info in the ROOT file. The first
"missing session sources entry" error still occurs, but it seems to
build the image anyway.
Email Gateway (Sep 27 2023 at 18:27):From: Makarius <makarius@sketis.net>
On 26/09/2023 22:43, Peter Lammich wrote:
I'm using afp-2023-09-26. With isabelle2023-RC5 and afp-devel 4605c928f00e
everything worked fine, so I didn't report that earlier.What is happening here? Is this caused by errors in the AFP entries, or am I
importing them the wrong way?
Log of build attempt: (ROOT and Scratch.thy attached to this email)
*** Consumer thread failure: "Isabelle.Session.manager"
*** Missing session sources entry
"~/devel/isabelle/afp-2023-09-26/thys/Separation_Algebra/sep_tactics.ML"
Finished Test (0:00:03 elapsed time, 0:00:06 cpu time, factor 1.89)
[...]
"/home/peter/.isabelle/Isabelle2023/browser_info/Unsorted/Test" ...
*** Missing session source file
"~/devel/isabelle/afp-2023-09-26/thys/Automatic_Refinement/Lib/Refine_Util_Bootstrap1.thy"
Just a quick guess from a distance, without trying to reproduce anything:
There could be something wrong with the conflation of source file names via
File.symbolic_path in Isabelle/Scala.
Repeatable results critically depend on process environment variables, e.g.
$AFP or $AFP_BASE for AFP. There are several variations on that theme. E.g. a
session .db file may end up with data using one variant, and later you try it
with another variant.
Note that you can check .db file content with the well-known sqlitebrowser
application (on any OS). The name of the SQL table is "isabelle_sources": If
that refers to anything different than your
~/devel/isabelle/afp-2023-09-26/thys path above, you need to rebuild the
sessions with extra care about AFP component settings etc.
Makarius
Email Gateway (Oct 17 2023 at 15:54):From: Peter Lammich <lammich@in.tum.de>
Using the AFP as a component, as described on the afp webpage solved the
problem.
before that, I had manually added it to ~/.isabelle/.../ROOTS, as I used
to do for years.
Last updated: Apr 28 2024 at 20:16 UTC