Dear all,
Unfortunately, Mirabelle is broken since aa8dce9ab8a9 ('discontinued
legacy load path;'). It relied on the implicit path, since it generates
a modified version of a theory file somewhere in /tmp, and then
processes that file using 'use_thy' in a raw isabelle_process. The
imports of the theory were found via the current working directory and
the implicit load path '.'.
Sascha and I tried three fixes which did not work:
a) add
ML_val {* Thy_Load.set_master_path ... *}
to the generated file. This works when processing the file interactively
in PG, but fails in batch mode, which seems to disallow ML commands
before the theory headers (and for a good reason, now that I think about
it...)
b) Set the master path in the corresponding ROOT.ML, before the use_thy
command. This has no effect, since use_thy of course resets the
master path.
c) Pipe the modified theory into 'isabelle tty', to simulate an
interactive session. Now setting the master path works, but the position
information from the original theory is lost. Mirabelle relies on the
line numbers to organize its results.
So I am wondering if the system could provide a variant of use_thy(s),
which takes an explicit master path and basically interprets the given
theory as if it would reside in that path. Probably, similar
functionality is already available for PG interaction. Of course any
other solution would be fine as well...
If all else fails, we could create the modified theory in the same
location as the original one, but poking in the original source
directories is likely to produce new problems, so it would be nice to
find another solution.
Any thoughts?
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
