Email Gateway (Aug 22 2022 at 18:03): 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
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: Nov 21 2024 at 12:39 UTC