Email Gateway (Aug 19 2022 at 14:37): Email Gateway (Aug 19 2022 at 14:37):From: Walther Neuper <wneuper@ist.tugraz.at>
Building our session "Isac" works very conveniently:
In "~~/ROOTS" we have an entry "src/Tools/isac" and in the latter
directory we have a "ROOT" (attached) with
session Isac in "~~/src/Tools/isac" = HOL + theories Build_Isac
and "Build_Isac.thy" (*); then in the commandline we execute "isabelle
jedit -l Isac" which builds the session automatically if an imported
file has been changed -- very convenient!
But generating theory browser information causes an ERROR: following
system.pdf we execute on the commandline:
(1)$ ./bin/isabelle build -o browser_info -v -c HOL
(2)$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v -b Isac
(1) works perfectly, (2) causes the error "Duplicate session "Isac"" (3) ---
--- where could we have introduced the "Duplicate session" ?
Walther
PS(3) the error message in full length:
neuper@neuper:/usr/local/isabisac$ ./bin/isabelle build -o browser_info
-d src/Tools/isac/ -v -b Isac
Started at Tue Jun 24 08:26:03 CEST 2014 (polyml-5.5.1_x86-linux on neuper)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/home/neuper/.isabelle/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
Duplicate session "Isac" (file "src/Tools/isac/ROOT")
Finished at Tue Jun 24 08:26:07 CEST 2014
0:00:04 elapsed time, 0:00:03 cpu time
ROOT
Email Gateway (Aug 19 2022 at 14:38):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Walther,
in the second command, you add your ROOT file twice to Isabelle's session directory (once
via ROOTS and once via "-d src/Tools/isac/". Isabelle does not realise that this is the
same specification and thus complains. Leave out the "-d ..." and it should work.
Andreas
Email Gateway (Aug 19 2022 at 14:38):From: Walther Neuper <wneuper@ist.tugraz.at>
On 06/24/2014 09:22 AM, Andreas Lochbihler wrote:
Hi Walther,
in the second command, you add your ROOT file twice to Isabelle's
session directory (once via ROOTS and once via "-d src/Tools/isac/".
Isabelle does not realise that this is the same specification and thus
complains. Leave out the "-d ..." and it should work.
Thanks a lot, Andreas --- deleting 3 characters is quick recovering from
lengthy studies of system.pdf ;-)))
Andreas
Walther
On 24/06/14 09:03, Walther Neuper wrote:
Building our session "Isac" works very conveniently:
In "~~/ROOTS" we have an entry "src/Tools/isac" and in the latter
directory we have a
"ROOT" (attached) withsession Isac in "~~/src/Tools/isac" = HOL + theories Build_Isac
and "Build_Isac.thy" (*); then in the commandline we execute
"isabelle jedit -l Isac"
which builds the session automatically if an imported file has been
changed -- very
convenient!But generating theory browser information causes an ERROR: following
system.pdf we execute
on the commandline:(1)$ ./bin/isabelle build -o browser_info -v -c HOL
(2)$ ./bin/isabelle build -o browser_info -d src/Tools/isac/ -v
-b Isac(1) works perfectly, (2) causes the error "Duplicate session "Isac""
(3) ------ where could we have introduced the "Duplicate session" ?
Walther
PS(3) the error message in full length:
neuper@neuper:/usr/local/isabisac$ ./bin/isabelle build -o
browser_info -d
src/Tools/isac/ -v -b Isac
Started at Tue Jun 24 08:26:03 CEST 2014 (polyml-5.5.1_x86-linux on
neuper)
ISABELLE_BUILD_OPTIONS=""ML_PLATFORM="x86-linux"
ML_HOME="/home/neuper/.isabelle/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"Duplicate session "Isac" (file "src/Tools/isac/ROOT")
Finished at Tue Jun 24 08:26:07 CEST 2014
0:00:04 elapsed time, 0:00:03 cpu time
Email Gateway (Aug 19 2022 at 14:38):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Andreas has beaten me to the punch. It's a duplication issue.
I think this might also be a duplicate of an issue that's been raised
before - on isabelle-dev by Christian Sternagel, then by myself, etc.
As I said last time, it would be nice if
isabelle/src/Pure/Tools/build.scala reported where it read the
duplicated addresses from. This makes it clear if there are conflicting
ROOT files, perhaps not quite as clear when a ROOT file is being
included twice (but clearer than guessing).
Well, that's just my 10 cents.
Cheers,
Thomas.
Last updated: Nov 21 2024 at 12:39 UTC