Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle + Alice


view this post on Zulip Email Gateway (Aug 18 2022 at 09:29):

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

view this post on Zulip Email Gateway (Aug 18 2022 at 09:29):

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: May 03 2024 at 08:18 UTC