Email Gateway (Jan 07 2022 at 12:04): Email Gateway (Jan 07 2022 at 12:04):From: Mac Goodwin <mgoodwin4@sheffield.ac.uk>
Hi,
I am trying to run an Isabelle theory file from the command line that
contains a short ML script that should write some exported code to disk.
Using the command isabelle process -T Calculator I receive the following
error:
*** Malformed command syntax
*** At command "<malformed>" (line 137 of
"/cygdrive/d/OneDrive/Documents/IsabelleDSL/Calculator.thy")
Exception- TOPLEVEL_ERROR raised
Line 137 is where the ML script begins. Is this the correct way to run an
isabelle file from the command line that contains an ML script? I have also
tried isabelle build -D . with a ROOT file (attached) which produces the
same error.
Thanks!
Mac
ROOT
Calculator.thy
Email Gateway (Jan 07 2022 at 22:46):From: Mac Goodwin <mgoodwin4@sheffield.ac.uk>
Hi Dominique,
Thank you very much for this - replacing the odd characters with < and >
gave a different but similar error ("ML source expected, but keyword < was
found") but your comment got me thinking along the lines of checking the ML
syntax was correct, and I found that wrapping the ML code inside {* and *}
fixed the issue!
Thanks very much for your help,
Mac
Email Gateway (Feb 28 2022 at 22:35):From: Mac Goodwin <mgoodwin4@sheffield.ac.uk>
Hi again,
Thanks for this advice, I've restructured my project as above and it works
a lot better this way. However, I am still unsure how to go from an export
inside the session, and Isabelle's file-system, to my disk. If I understand
correctly, the 'export artifacts' you described above are not saved to disk
Is this possible using the build options as described? I can successfully
run and export my 'code' with isabelle build -e -D ., but as far as I can
tell this doesn't allow further processing of the Haskell files that
export_code within Isabelle has produced.
As for the cartouche syntax - I have replaced my incorrect syntax with the
cartouche as suggested, but still see this error when attempting to build:
$ isabelle build -e -D .
Running Calculator ...
Calculator FAILED
(see also
C:\Users\theco\.isabelle\Isabelle2021\heaps\polyml-5.8.2_x86_64_32-windows\log\Calculator)
*** Malformed command syntax
*** At command "<malformed>" (line 137 of
"/cygdrive/d/OneDrive/Documents/IsabelleDSL/Calculator.thy")
Line 137 here is the beginning of the ML script I originally used to export
code to disk. The script works with the old style syntax, but I'd love to
change it to make it work better within Isabelle best practices.
Best wishes,
Mac
On Sat, 22 Jan 2022 at 14:27, Makarius <makarius@sketis.net> wrote:
On 06/01/2022 14:55, Mac Goodwin wrote:
Using the command
isabelle process -T CalculatorI receive the
following error:Is this the correct way to run an
isabelle file from the command line that contains an ML script? I have
also
triedisabelle build -D .with a ROOT file (attached) which produces
the
same error.Note that "isabelle process" is a very low-level way to experiment with an
ML
process that lacks a proper session context. Many things just don't work
here;
you should avoid it in "production use".A proper "isabelle build" with ROOT is much better.
Instead of writing out things to the physical file-system, you should work
with the export artifacts for the session. In Isabelle/ML this is done via
Export.export (and derivatives), in Isabelle/Scala there are operations to
retrieve results from the corresponding session build database: it is like
a
formal file-system for the session (and not a "disk").There is also "isabelle export" to access exports from the command-line,
e.g.
"isabelle export -l My_Session". Moreover the "system" manual explains
'export_files' within session ROOT specifications in chapter 2 "Isabelle
sessions and build management".Makarius
Email Gateway (Apr 08 2022 at 15:08):From: Mac Goodwin <cl-isabelle-users@lists.cam.ac.uk>
For anyone with a similar use case/issue, I eventually got this working
with the following setup:
In the ROOT file for the project, add an export_files statement as per
system manual: export_files (in ".") ":*.hs"
This outputs exports *to *the current directory (indicated by ".") and
filters for haskell files (":*.hs").
Given an export_code command in your theory file (such as "export_code
function in Haskell module_name Calculator file_prefix calculator") it is
then possible to retrieve the exported code from Isabelle's virtual file
system using the following command to build, and then export, the files:
isabelle export -d . -x ":*.hs" [SESSION_NAME]
Where SESSION_NAME is the session name specified in your ROOT file. This
command should be run from the same directory as the ROOT file and theory
file.
This setup then eliminates the need for ML code. For some quick feedback -
I think the system manual could do with a few more worked examples of how
to chain these commands together! As a beginner Isabelle user, I personally
found it a bit confusing. I did find the Code Generation paper useful when
figuring this out: https://isabelle.in.tum.de/doc/codegen.pdf
Thanks,
Mac
Last updated: Jul 15 2022 at 23:21 UTC