Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] exceptions in theory files that use ML files

Email Gateway (Aug 18 2022 at 13:40):

From: Lucas Dixon <ldixon@inf.ed.ac.uk>
If I have a theory file which starts:

theory PureIsaP
imports HOL
uses "src/build/Pure_IsaP.ML"
begin

The file "Pure_IsaP.ML" uses a number of other files. I noticed that
when an exception is raised, I get something like this:

*** exception SysErr of ("chdir failed", SOME ENOENT) raised
*** val d = "/home/ldixon/work/IsaP/trunk/IsaPlanner" : string
*** val it = () : unit
*** val it = () : unit
*** val it = () : unit
*** val it = () : unit
*** Exception- TOPLEVEL_ERROR raised
*** At command "theory".

However, this doesn't tell me in which sub-file the exception was
raised. Any suggestions?

thanks,
lucas

Email Gateway (Aug 18 2022 at 13:40):

From: Makarius <makarius@sketis.net>
Maybe the exception trace produced by Toplevel.debug := true provides some
extra hints.

Anyway, if this is more that just an experiment, you need to specify all
loaded ML files in the theory header, via uses ("my_extra_file.ML") with
parentheses. This means it is usually easier to use all files directly
from the header in the first place, see the start of src/HOL/HOL.thy for
example.

Makarius

Email Gateway (Aug 18 2022 at 13:41):

From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Makarius wrote:

On Tue, 30 Jun 2009, Lucas Dixon wrote:

If I have a theory file which starts:

theory PureIsaP
imports HOL
uses "src/build/Pure_IsaP.ML"
begin

The file "Pure_IsaP.ML" uses a number of other files. I noticed that
when an exception is raised, I get something like this:

*** exception SysErr of ("chdir failed", SOME ENOENT) raised
*** val d = "/home/ldixon/work/IsaP/trunk/IsaPlanner" : string
*** val it = () : unit
*** val it = () : unit
*** val it = () : unit
*** val it = () : unit
*** Exception- TOPLEVEL_ERROR raised
*** At command "theory".

However, this doesn't tell me in which sub-file the exception was
raised. Any suggestions?

Maybe the exception trace produced by Toplevel.debug := true provides
some extra hints.

So, to try this, should I change my theory file header to:

theory PureIsaP
imports HOL
uses ("src/build/Pure_IsaP.ML")
begin
ML{* Toplevel.debug := true; *}
use "src/build/Pure_IsaP.ML";

I cannot call ML code outside of a theory, this means I have to move
test code like that into the theory, as above, right?

Having tried this, I found it still didn't tell me the file being
executed that raised the exception, although it did (if I understand it
correctly) tell me the file which contains the function that raised the
exception (it was library.ML). It also gave me an exception trace, but
that wasn't useful in this case:

ML_Context.exec(2)
Toplevel.generic_theory(1)(1)(1)
Runtime.debugging(2)(1)
End of trace

Anyway, if this is more that just an experiment, you need to specify
all loaded ML files in the theory header, via uses
("my_extra_file.ML") with parentheses.

This means it is usually easier
to use all files directly from the header in the first place, see the
start of src/HOL/HOL.thy for example.

OK, I guess I can do that. Maybe a good thing to say in the Isabelle
Cookbook.

If possible, it would be good to have a solution that can reflect the
structure of code. I have several collections of files which make sense
to be loaded together (over 100 files altogether). In ML files, I
previously had a collection of different ROOT.ML files which loaded the
appropriate sub ROOT.ML files, thus providing some structure to the
various modules. I guess I can do this by having a theory for each code
module instead of my old ROOT.ML files ?

cheers,
lucas

Email Gateway (Aug 18 2022 at 13:41):

From: Makarius <makarius@sketis.net>
On Tue, 30 Jun 2009, Lucas Dixon wrote:

So, to try this, should I change my theory file header to:

theory PureIsaP
imports HOL
uses ("src/build/Pure_IsaP.ML")
begin
ML{* Toplevel.debug := true; *}
use "src/build/Pure_IsaP.ML";

I cannot call ML code outside of a theory, this means I have to move test
code like that into the theory, as above, right?

Regular 'ML' needs a context, because it can emit toplevel bindings, which
are stored there. You can always say 'ML_val' or 'ML_command', even
before the initial 'theory' (in interactive mode).

Having tried this, I found it still didn't tell me the file being
executed that raised the exception, although it did (if I understand it
correctly) tell me the file which contains the function that raised the
exception (it was library.ML). It also gave me an exception trace, but
that wasn't useful in this case:

Since you are using the repository versions of Poly/ML and Isabelle (both
moving very fast), you should in principle get a detailed trace for the
nested ML invocation, as well as a file/line position for the last
exception (but that is probably just that of the "error" function in
library.ML).

On the other hand, things might be broken right now. Or the situation
might be a bit different than expected. Which "chdir" did you use? Our
"cd" or a different version?

If possible, it would be good to have a solution that can reflect the
structure of code. I have several collections of files which make sense
to be loaded together (over 100 files altogether). In ML files, I
previously had a collection of different ROOT.ML files which loaded the
appropriate sub ROOT.ML files, thus providing some structure to the
various modules.

We used to have this for src/Pure until recently. Now there is only a
single flat ROOT.ML without any chdirs. This was motivated by precise
source file tracking of Poly/ML 5.3pre, but has also clarified our load
process.

I guess I can do this by having a theory for each code module instead of
my old ROOT.ML files ?

You could do that. In main HOL it happens all the time, although it is
due to actual intermediate theory development before further ML files can
be loaded.

Makarius

Last updated: May 03 2024 at 12:27 UTC