Re: [isabelle] Running ML in a theory context from the command line



> https://github.com/isabelle-prover/opentheory-component

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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.