Email Gateway (Aug 22 2022 at 09:08): Email Gateway (Aug 22 2022 at 09:08):From: Walther Neuper <wneuper@ist.tugraz.at>
Makarius,
thank you for investing your precious time now (before the next Isabelle
release) into my nasty questions ...
I interpret "modular components" like that:
wneuper@ProBook:/usr/local/Isabelle2014$ ### Building Isabelle/jEdit ...
Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component
tried another build
wneuper@ProBook:/usr/local/Isabelle2014$ ./bin/isabelle jedit -l HOL &
[2] 21912
wneuper@ProBook:/usr/local/Isabelle2014$ ### Building Isabelle/Scala ...
Changed files:
Concurrent/consumer_thread.scala
:
../Tools/Graphview/src/visualizer.scala
wneuper@ProBook:/usr/local/isabisac$ ### Building Isabelle/jEdit ...
Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component
Here I stopped my trials for another question, where you are probably
the only person to answer it: In the meanwhile I found out, that the
Isabelle installation on my computer behaves coherently:
wneuper@ProBook:~/proto3$ ./repos/isac-java/src/java/properties/START_ISABELLE
Unknown Isabelle tool: tty
where the script "START_ISABELLE", called from Java, is a plain
"isabelle tty ..."
So my question: Can we run Isabelle2013-2 and Isabelle2014 in parallel
on one computer?
And if yes: How do we do that?
Walther
Email Gateway (Aug 22 2022 at 09:11):From: Makarius <makarius@sketis.net>
Such adhoc merges merely produce a Mercurial swamp. Clear-cut modular
structure is something different.
I can't say anything specific, without seeing the merged and modified
repository content. The cumulative diff against a define point from our
side might help, but the diff might be also quite large.
Makarius
Email Gateway (Aug 22 2022 at 09:40):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi,
After studying system.pdf several times and now for a while, I cannot
come to a clue and give an exhaustive protocol of what I'm doing --
sorry for the long ist.
(1) According to ~~/README_REPOSITORY I follow pt.2 Clone repository,
and the cloned Isabelle2014 runs perfectly.
(2) Then I need to merge with our local development and see, that the
previously running installation is broken:
/usr/local/isabisac$ ./bin/isabelle jedit -l HOL
Unknown Isabelle tool: env
(3) So I retry
/usr/local/isabisac$ ./bin/isabelle components -I
/usr/local/isabisac$ ./bin/isabelle components -a
/usr/local/isabisac$ ./bin/isabelle jedit -l HOL
Unknown Isabelle tool: env
(4) And then I get stuck, because I cannot even clean:
/usr/local/isabisac$ ./bin/isabelle build -c
Unknown Isabelle tool: env
What can I do to get the "Isabelle tool: env" known (*)?
Walther
PS: During the above mentioned merge I noticed, that ~~/ROOTS had lost
the entry "src/Tools/", but the above trials were run with this entry
reestablished.
(*) There is also no matching "Unknown Isabelle tool: env" in the
mailarchive, and I cannot relate "Unknown Isabelle tool" to my problem,
sorry.
Email Gateway (Aug 22 2022 at 09:41):From: Makarius <makarius@sketis.net>
On Sat, 11 Apr 2015, Walther Neuper wrote:
After studying system.pdf several times and now for a while, I cannot come to
a clue and give an exhaustive protocol of what I'm doing -- sorry for the
long ist.(1) According to ~~/README_REPOSITORY I follow pt.2 Clone repository, and
the cloned Isabelle2014 runs perfectly.(2) Then I need to merge with our local development and see, that the
previously running installation is broken:
The "need to merge" is the deeper problem here. Collecting many adhoc
changes of the Isabelle repository an merging the whole new history over
and over again eventually leads to a big mess.
I don't think a merge is needed at all. Isabelle is so modular wrt. its
"components" that any tool out there should be able to fit into an
official Isabelle version without adhoc changes. If not, I would like to
see explicit counter-examples, which can then be eliminated.
/usr/local/isabisac$ ./bin/isabelle jedit -l HOL
Unknown Isabelle tool: envPS: During the above mentioned merge I noticed, that ~~/ROOTS had lost
the entry "src/Tools/", but the above trials were run with this entry
reestablished.(*) There is also no matching "Unknown Isabelle tool: env" in the
mailarchive, and I cannot relate "Unknown Isabelle tool" to my problem,
sorry.
Isabelle command-line tools are collected from ISABELLE_TOOLS within the
Isabelle environment. This is produced by the available components. The
"env" tool is so elementary that it is in $ISABELLE_HOME/lib/Tools -- if
that is not accessible, hardly anything should work.
Makarius
Last updated: Apr 23 2024 at 12:29 UTC