Email Gateway (Aug 18 2022 at 18:32): Email Gateway (Aug 18 2022 at 18:32):From: Matthew <superuser@mattweidner.com>
In the first step of building an automatic tool, I am trying to set up
an Isar-level command, following the example of the Nitpick sources.
However, I am having a problem getting Isar to "see" the command.
Here is an utterly simplified version, based on the Nitpick sources.
File test.ml
signature TEST =
sig
end
structure Test : TEST =
struct
fun test_function a =
writeln( "test function called" )
|> K(K(Toplevel.empty),a)
fun test_params_function a =
writeln( "test params function called" )
|> K(K(Toplevel.empty),a)
val _ = Outer_Syntax.improper_command "test"
"test the Outer_Syntax.improper_command function"
Keyword.diag test_function
val _ = Outer_Syntax.command "test_params"
"test the Outer_Syntax.command function"
Keyword.thy_decl test_params_function
end
End file test.ml
As far as I can tell, the following Isar code should load the commands
"test" and "test_params" into Isar's syntax:
theory Scratch
imports Main
uses ("test.ml")
begin
use "test.ml"
However, if I next type test or test_params and try to process it,
ProofGeneral will protest that it cannot find any complete commands to
process.
What am I doing wrong here?
Thanks,
Matthew Weidner
Email Gateway (Aug 18 2022 at 18:32):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello Matthew,
the details how to set up a command properly are explained in great
detail in "The Isabelle Cookbook"
(http://isabelle.in.tum.de/nominal/activities/idp/) in chapter 5.8 (page
98 ff.)
Hope this helps.
Lukas
Email Gateway (Aug 18 2022 at 18:32):From: Makarius <makarius@sketis.net>
Here are some general hints:
* Isabelle/ML files should always have an .ML extension, not .ml or .sml
* Small ML things are more easily develepd directly in ML {* ... *}
chunks within a theory.
* Proof General requires commands declared statically in a keyword
file. It was already pointed out that the cookbook by Christian Urban
provides some hints on that.
* The Isabelle/jEdit Prover IDE, which is particulaly nice for ML
development (as of Isabelle2011-1), requires some trickery though
to make it accept newly created Isar commands dynamically at runtime.
* K(K(Toplevel.empty),a) is an odd way to make an outer parser that
produces an Isar toplevel transition. Where did you see the example?
Here is my version of your test. It imitates some of the basic print
commands in ~~/src/Pure/Isar/isar_syn.ML (the file where the main
Isabelle/Pure commands are defined):
ML {*
val _ =
Outer_Syntax.improper_command "test" "test command" Keyword.diag
(Scan.succeed
(Toplevel.no_timing o Toplevel.imperative (fn () => writeln "test")));
*}
Above I have inlined the parser expression and the construction of the
toplevel transaction into the command definition. This is more robust
wrt. type inference issues than a bottom-up sequence of auxiliary building
blocks like test_function above. (That form was preferred in a time where
Poly/ML produced very bad type error messages for combinator expressions.)
Makarius
Email Gateway (Aug 18 2022 at 18:32):From: Christian Urban <urbanc@in.tum.de>
Hi,
Makarius writes:
* The Isabelle/jEdit Prover IDE, which is particulaly nice for ML
development (as of Isabelle2011-1), requires some trickery though
to make it accept newly created Isar commands dynamically at runtime.
Out of interest, how does this trickery work concretely?
Thanks,
Christian
Email Gateway (Aug 18 2022 at 18:33):From: Holger Gast <gast@informatik.uni-tuebingen.de>
Dear Matthew,
You can always use I3P (http://www-pu.informatik.uni-tuebingen.de/i3p/).
Besides being fast and extensible, it also handles dynamically defined
commands.
BTW, as for the previous Isabelle releases,
the driver for Isabelle2011-1 is ready and tested.
Also, following several requests, I have made the development
repository public (see web-page).
Last updated: Apr 25 2024 at 12:23 UTC