From: Priya Gopalan <priya.g@ed.ac.uk>
Hello,
I am trying to get Isabelle2005 to work with Alice, a functional
programming language based on Standard ML, extended with rich support
for concurrent, distributed, and constraint programming.
http://www.ps.uni-sb.de/alice/
Does anyone have any experience on attempting something on these lines,
i.e, getting Isabelle2005 to work on a non-standard ML flavour?
I will be grateful to hear any useful info on this: any tweaks that
will help etc.
Many Thanks,
Priya
From: Tjark Weber <tjark.weber@gmx.de>
Priya,
I assume you are aware of the recommendations given on
http://www.ps.uni-sb.de/alice/manual/incompatibilities.html.
Isabelle already supports a number of ML systems. See the etc/settings file
for some options, and Chapter 1 of the Isabelle System Manual [1] for
documentation. Also have a look at the startup scripts in
Distribution/lib/scripts.
Incomplete library structures (like those mentioned on
http://www.ps.uni-sb.de/alice/manual/limitations.html) are something that we
have encountered before. Perhaps you are lucky that Isabelle doesn't
actually use any of the missing functionality. Otherwise you may find the
files in Pure/ML-Systems helpful.
Best,
Tjark
[1] http://isabelle.in.tum.de/dist/Isabelle/doc/system.pdf
Last updated: Nov 21 2024 at 12:39 UTC