Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ad: run heap with minimal effort in Isabelle20...

Email Gateway (Aug 19 2022 at 16:36):

From: Walther Neuper <wneuper@ist.tugraz.at>
The theories and ML-files of our project are managed in a session Isac,
which creates a heap with the same name.

We try to make installation easy for users such that they

create an Isabelle standard installation

copy the Isac binary to the place where the Pure- and HOL-binaries reside.

Now we want to start from a shell by

Isabelle2013-2/bin$ ./isabelle jedit -l Isac &

and get the message

Undefined session(s): "Isac"

Is there a way to trick out the ROOT(S) in Isabelle2013-2? If yes, how?

Walther

Email Gateway (Aug 19 2022 at 16:37):

From: Makarius <makarius@sketis.net>
There is no need for tricks -- there are many official ways.

The most basic one is to add a suitable -d option the the isabelle jedit
command line above, and then have ROOT or ROOTS entries within that
directory.

Another possibility is to make an Isabelle component that provides its own
ROOT/ROOTS hierarchy. Examples for such components may be found via
"isabelle components -l".

The "system" manual describes in further detail how things work.

Makarius

http://stop-ttip.org 851,662 people so far

Last updated: Nov 21 2024 at 12:39 UTC