[isabelle-dev] Mirabelle and load path

[Alexander Krauss]

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