Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help us trial web interfaces to Isabelle


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

From: William Billingsley <whb21@cam.ac.uk>
We are working web-based interfaces for proof exercises using Isabelle,
and we'd appreciate your help in assessing their usefulness and usability.

Two small prize draws will be made for those taking part and responding
to the questionnaires about the interfaces.

We are trialling two kinds of interface. One uses Isar, and the other
uses MathsTiles (a way of writing proofs that vaguely resembles how a
student might write it on paper). They are hosted as exercises in an
"Intelligent Book" - a kind of web-based textbook.

The Isar interface is available today, at
http://www.discmath.cl.cam.ac.uk/DiscreteMathsBook
Under the column "Experiment for Isabelle Experts".
(you'll need to register first so we can get a unique name for you)

The MathsTiles interface will be made available in the next 24 hours or
so, also at
http://www.discmath.cl.cam.ac.uk/DiscreteMathsBook
Under the column "Experiment for Everybody"

The exercises use Java applets, so you will need the Java plugin version
1.5 or higher for your browser. This is available from java.sun.com
We have tested on Internet Explorer (Windows) and Mozilla Firefox
(Windows/Linux), but we haven't tested using Safari.

Any questions, problems, or bugs, please email me at whb21@cam.ac.uk

Thank you very much if you are willing to help by taking part.

Will Billingsley
PhD student
Intelligent Book project


Last updated: May 03 2024 at 04:19 UTC