[isabelle] Help with using AFP from Isabelle on Windows

[王淑灵]

Dear Isabelle users,

I want to use AFP theories in my formalization and have downloaded the AFP directory to /Isabelle2017. I am using Isabelle/HOL on windows. So I run Cygwin-Terminal under Isabelle2017 directory, and run the following command:

echo /afp/thys >> ROOTS

but it says “bash: ROOTS: Permission denied”

Any solution please? Thank you very much for your help.

Best,
Shuling

Best regards,
Shuling Wang
SKLCS, Institute of S

[Stefan Berghofer]

Post by 王淑灵
Dear Isabelle users,
echo /afp/thys >> ROOTS
but it says “bash: ROOTS: Permission denied”
Any solution please? Thank you very much for your help.
Best,
Shuling

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

[Makarius]

Post by 王淑灵
echo /afp/thys >> ROOTS
but it says “bash: ROOTS: Permission denied”

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