Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Help with using AFP from Isabelle on Windows


view this post on Zulip Email Gateway (Aug 22 2022 at 18:03):

From: Stefan Berghofer <berghofe@in.tum.de>
Dear Shuling,

it is not particularly surprising that you get this error message, since ROOTS is not an executable, but a list of
directories containing ROOT files (see e.g. the explanation of the -d command line option in section 2.3
of the Isabelle System Manual). If you want to process a theory that depends on some theory in the AFP using
Isabelle/jEdit, you can use the following command

isabelle jedit -d <path to AFP installation directory>/thys My_Theory.thy

where My_Theory.thy looks e.g. as follows:

theory My_Theory
imports "Example-Submission.Submission"
begin

thm very_true

end

Greetings,
Stefan

view this post on Zulip Email Gateway (Aug 22 2022 at 18:06):

From: Makarius <makarius@sketis.net>
First of all you should use the current release Isabelle2018 (August
2018), not the old Isabelle2017.

Note that the Cygwin-Terminal starts in the main Isabelle directory, so
the above error means that $ISABELLE_HOME/ROOTS file is not writable.
This can mean that another user has installed Isabelle and it is
read-only for your own account.

You can always edit $ISABELLE_HOME_USER/ROOTS (using that file name
literally in Isabelle/jEdit). It even has a template with some comments.

In particular, you need to use Isabelle path notation, for example:

/cygdrive/c/Users/wenzelm/afp-2018/thys

Moreover note that activating all of AFP like that delays the startup of
the Isabelle/jEdit application considerably, especially on Windows.

You can also put specific sub-directories of afp-2017/thys in ROOTS, but
you will have to resolve dependencies between entries manually. The
Prover IDE should do this at some point for the user.

Makarius


Last updated: Mar 29 2024 at 08:18 UTC