Email Gateway (Aug 22 2022 at 17:04): Email Gateway (Aug 22 2022 at 17:04):From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Greetings,
I want to get, from a single Isabelle theory-file (from now on called
"working .thy file") the latex code to display it with pdfLaTeX. After
following the Isabelle's System Manual/wiki on latex code-snippets
<https://isabelle.in.tum.de/community/Generate_TeX_Snippets>; creating the
ROOT documents to handle sessions; checking that there is nothing wrong
with my LaTeX setting, and entering the command "isabelle build -D
aSessionName", the system complains and says:
"No such file:
/blah..blah/working_directory/Ord_Diff_Eqtns/Initial_Value_Problem.thy"
For a summary of my configuration, here is a diagram, where "depends on"
means that a .thy file "imports" another one in the pointed directory:
So, when I copied the Ord_Diff_Eqtns-entry of the AFP into my
working_directory, the error disappeared; but another one was shown:
"No such file:
/blah..blah/working_directory/Ord_Diff_Eqtns/Arithmetic/Executable_Euclidean_Space.thy"
This was just a "bad-error" because in the AFP, the affine-arithmetic-entry
should not be inside the ODEs-entry. Again if I move the affine-arithmetic
directory inside the ODE's one, then a similar error of the next dependency
shows up.
How could I get rid of all this errors?
Captura de pantalla 2018-04-10 a la(s) 13.32.45.png
Email Gateway (Aug 22 2022 at 17:04):From: Makarius <makarius@sketis.net>
imports with directory locations instead qualified theory names (newly
introduced in Isabelle2017).
You should make sure that:
* all imports from another session use a qualified theory name:
"My_Session.My_Theory"
* all imported sessions are declared as "sessions" in the ROOT entry
* all project directories (with session ROOT and ROOTS) are given as
options -d to "isabelle build" or are persistently enabled in
$ISABELLE_HOME_USER/ROOTS for example.
Mixing old-style (dir + file names) and new-style (session-qualified
names) theory imports should be avoided at all cost. The "isabelle
imports" tool helps to achieve this uniformly (see NEWS and "system"
manual), but it sometimes requires manual refinement of the result.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC