Created attachment 300003 [details, diff] make isabelle ebuild install configuration files in /etc/isabelle, not /etc/isabelle/etc When running isabelle, this happens for me: > isabelle > > Usage: isabelle NAME [ARGS ...] > > Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. > > Available tools are: > Use of uninitialized value in split at /usr/share/Isabelle2011-1/lib/scripts/tools.pl line 12. What isabelle does not tell at this point: it could not find any of its configuration files. It was looking for them in /etc/isabelle/etc instead of /etc/isabelle. If there are no objections, I suggest this fix: diff -ur a/isabelle-2011.1.ebuild b/isabelle-2011.1.ebuild --- a/isabelle-2011.1.ebuild 2012-01-26 21:00:20.000000000 +0100 +++ b/isabelle-2011.1.ebuild 2012-01-26 20:49:41.000000000 +0100 @@ -109,7 +109,7 @@ dodir /etc/isabelle insinto /etc/isabelle - doins -r etc + doins -r etc/* dosym /etc/isabelle "${TARGETDIR}/etc" dosym "${LIBDIR}/heaps" "${TARGETDIR}/heaps" (this patch is also attached in a separate file)
Sorry, I wrote it the wrong way round: > It was looking for them in /etc/isabelle/etc instead of /etc/isabelle. That is wrong. It should read: > It was looking for them in /etc/isabelle instead of /etc/isabelle/etc. Anyway. This does not change anything on the problem or the fix.
Committed proposed fix, thanks for the report and fix! After emerge sci-mathematics/isabelle with the fix, the output of running isabelle is: % isabelle Usage: isabelle NAME [ARGS ...] Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help. Available tools are: browser - Isabelle graph browser dimacs2hol - convert DIMACS CNF files into Isabelle/HOL theories display - display document (in DVI or PDF format) doc - view Isabelle documentation document - prepare theory session document emacs - Proof General / Emacs interface wrapper env - run a program in a modified environment findlogics - collect heap names from ISABELLE_PATH getenv - get values from Isabelle settings environment install - install standalone Isabelle executables java - invoke Java within the Isabelle environment keywords - generate outer syntax keyword files from session logs latex - run LaTeX (and related tools) logo - create an instance of the Isabelle logo make - Isabelle make utility makeall - apply make utility to all logics mkdir - prepare logic session directory mkproject - prepare a session directory for PG-Eclipse print - print document scala - invoke Scala within the Isabelle environment scalac - invoke Scala compiler within the Isabelle environment tty - run Isabelle process with plain tty interaction unsymbolize - remove unreadable symbol names from sources usedir - build object-logic or run examples version - display Isabelle version yxml - simple XML to YXML converter %
