Email Gateway (Aug 22 2022 at 17:20): Email Gateway (Aug 22 2022 at 17:20):From: Lars Hupel <hupel@in.tum.de>
Dear list,
with the help of Makarius and Joe Hurd, OpenTheory can now be fully
loaded into Isabelle/Pure:
https://github.com/isabelle-prover/opentheory-component
Inside an interactive environment, e.g. Isabelle/jEdit, it is possible
to call the tool via "Open_Theory.main".
I am trying to figure out if this can also be done from the command
line, as an Isabelle tool. There's already precedent, e.g. the various
"tptp" tools from Jasmin.
In "tptp_sledgehammer", for example, a theory file is constructed that
imports some root theory and contains an ML snippet. It is then called
via "isabelle process". This of course works, but I was wondering
whether there's a more direct way, e.g. with "isabelle process -e". But
I'm not sure what the correct incantation is to make it evaluate the ML
snippet in the context of a theory, so that the "Open_Theory" structure
is available.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:21):From: Makarius <makarius@sketis.net>
The following is derived from the definition of 'ML_command':
fun eval_in_theory thy s =
ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
ML_Compiler.flags (Input.string s);
Here is a complete example (with the included Scratch.thy):
isabelle process -l Pure -T "~/Scratch" -e "fun eval_in_theory thy s =
ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
ML_Compiler.flags (Input.string s)" -e 'eval_in_theory
(Thy_Info.get_theory "Draft.Scratch") "test (serial_string ())"'
Maybe I should provide a function line eval_in_theory already in Pure.
Are there further important applications?
Makarius
Scratch.thy
Email Gateway (Aug 22 2022 at 17:21):From: Lars Hupel <hupel@in.tum.de>
Here is a complete example (with the included Scratch.thy):
isabelle process -l Pure -T "~/Scratch" -e "fun eval_in_theory thy s =
ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
ML_Compiler.flags (Input.string s)" -e 'eval_in_theory
(Thy_Info.get_theory "Draft.Scratch") "test (serial_string ())"'
Thanks, that should work.
Maybe I should provide a function line eval_in_theory already in Pure.
Are there further important applications?
I suppose all of the "tptp" tools, they use the same trick with a
temporary file. But Jasmin could say for sure.
Email Gateway (Aug 22 2022 at 17:21):From: Lars Hupel <hupel@in.tum.de>
This is now available as a stand-alone Isabelle component. The
repository above has installation instructions.
Proof that it works:
$ isabelle-dev opentheory
val eval_in_theory = fn: string -> string -> unit
opentheory: no command specified
usage: opentheory [global options] command [command options] INPUT ...
where the available commands are:
opentheory cleanup ..... clean up packages staged for installation
opentheory export ...... export an installed package
opentheory help ........ display help on all available commands
opentheory info ........ extract information from packages and files
opentheory init ........ initialize a new package repo
opentheory install ..... install a package from a theory file or repo
opentheory list ........ list installed packages
opentheory uninstall ... uninstall packages
opentheory update ...... update repo package lists
opentheory upgrade ..... upgrade packages with later versions on a repo
opentheory upload ...... upload installed packages to a repo
Displaying global options:
-d, --root-dir DIR ... set package repo directory
--repo REPO .......... use given remote package repo
--show-types ......... annotate every term variable with its type
-- ................... no more options
-?, -h, --help ....... display option information and exit
-v, --version ........ display version information
Exception- ERROR "exception Exit ? raised (line 15 of
\"~/work/opentheory/opentheory-component/Open_Theory.thy\")" raised
There's no use case yet, this is just a proof of concept.
Last updated: Apr 25 2024 at 08:20 UTC