Re: [isabelle] Unknown Isabelle tool: env



Makarius,

thank you for investing your precious time now (before the next Isabelle release) into my nasty questions ...

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.

I interpret "modular components" like that:
# copied the merged ".hg/" and "src" into "Isabelle2014"
# tried to build

wneuper at ProBook:/usr/local/Isabelle2014$ ### Building Isabelle/jEdit ...
   Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component

# copied "Admin/" from an Isabelle2014 clone into "Isabelle2014" and tried another build

wneuper at ProBook:/usr/local/Isabelle2014$ ./bin/isabelle jedit -l HOL &
   [2] 21912
   wneuper at ProBook:/usr/local/Isabelle2014$ ### Building Isabelle/Scala ...
   Changed files:
     Concurrent/consumer_thread.scala
     :
     ../Tools/Graphview/src/visualizer.scala
   wneuper at 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 at 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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.