Re: [isabelle-dev] Two problems
On Mon, 3 Dec 2012, Jasmin Christian Blanchette wrote:
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
begin
nondeterministically gives either
*** Undeclared type constructor: vname (line 12 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
*** Failed to parse type
*** in type abbreviation fdecl
*** At command type_synonym (line 11 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
or
*** Inner lexical error at: ⟪i:U⟫ ⊢ t : T ⟹
*** IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i]) (line 91 of
~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
*** Failed to parse proposition
*** At command lemma (line 90 of ~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
but each of them loads fine on its own.
Proof General uses the theory loader of the TTY, and that has certain
features. There used to be a toplevel load path, with directories
searched in a certain order, and the first fit was taken. Later that was
found useful in the imports part as well, but it causes odd effects until
today: your imports are somehow non-authentic and non-compositional.
Having theory Type via one part of the import graph already, it is not
imported again just because some file happens to be around in a different
directory.
In recent years I've worked towards sorting out many such odd effects.
The master directory instead of load path was already some
improvement.
In your observations above, are you sure that nondeterministically means
physical nondeterminism, say due to parallel loading of theories? Or
theories that you have visited before in Proof General, before starting
the above one?
My hope and expectation for the classic theory loader is that it first
explores the whole graph as specified in the imports list. Then it starts
loading in parallel. Shuffling imports a little may change the order of
theory discovery and loading, but with given struture specified in the
theory sources it should be deterministic (although sometimes surprising).
Note that Isabelle/jEdit handles this a bit differently. The full master
path is taken into account for theory source identification. Later there
is the classic check of consistent naming that produces this error in the
above example:
exception THEORY raised (line 325 of context.ML):
Inconsistent theory versions
{..., Nitpick, Main, Lambda, ListApplication, Type}
{..., Predicate_Compile, Nitpick, Main, Aux, Type}
Testing a bit further, I've actually discovered a dropout stemming from
Dec-2008: clashes on the imports list itself were not rejected like that.
This is now addressed in Isabelle/955c4aa44f60. (Luckily the externally
visible names are not relevant for the integrity of the nano kernel,
only the internal ids.)
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
On Mon, 3 Dec 2012, Lawrence Paulson wrote: Surely the existence of two theories of the same name can be detected? The deeper problem here is that theories still have the ancient flat name space. So the file-system paths in the source are ultimately stripped to the base name when doing comparisons. We are still moving (extremely slowly) towards fully-qualified theory names of the form SESSION.THEORY, e.g. HOL.Main, HOLCF.HOLCF with some ways to omit the prefix within the same session, say. The isabelle build reform from this summer already introduces an authentic name space for (unqualified) session names. Here are some of the remaining obstacles to prefix session names to theory names: * Too many ways to manage theory dependencies. There are old and new theory loader variants and combinations: isabelle tty, build, emacs, jedit all do it slightly differently. Ultimately, I would like to see just one way in Isabelle/Scala, and even Proof General would use that without taking notice. * Proof tools that assume that the long names for formal entities look like this: THEORY.NAME THEORY.LOCALE.NAME Larry himself introduced this assumption some years ago, but it was not there in 1998 when I introduced the name space concept in Isabelle. ML tools should not guess at the layout of full names. This is an abstract datatype that happens to be implemented as string for historical reasons. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Am 08.12.2012 um 14:07 schrieb Makarius: In your observations above, are you sure that nondeterministically means physical nondeterminism, say due to parallel loading of theories? Or theories that you have visited before in Proof General, before starting the above one? Each time I clicked Exit Isabelle, so it seemed to depend on how fast the two theories were loaded. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Of course a full solution might be a lot of work. But merely to detect the presence of two identically-named theories (in the spirit of detecting instances of a variable with two different types) might be straightforward, even if the only response is a fatal error. Since otherwise the outcome might be very confusing. Larry On 8 Dec 2012, at 13:18, Makarius makar...@sketis.net wrote: On Mon, 3 Dec 2012, Lawrence Paulson wrote: Surely the existence of two theories of the same name can be detected? The deeper problem here is that theories still have the ancient flat name space. So the file-system paths in the source are ultimately stripped to the base name when doing comparisons. We are still moving (extremely slowly) towards fully-qualified theory names of the form SESSION.THEORY, e.g. HOL.Main, HOLCF.HOLCF with some ways to omit the prefix within the same session, say. The isabelle build reform from this summer already introduces an authentic name space for (unqualified) session names. Here are some of the remaining obstacles to prefix session names to theory names: * Too many ways to manage theory dependencies. There are old and new theory loader variants and combinations: isabelle tty, build, emacs, jedit all do it slightly differently. Ultimately, I would like to see just one way in Isabelle/Scala, and even Proof General would use that without taking notice. * Proof tools that assume that the long names for formal entities look like this: THEORY.NAME THEORY.LOCALE.NAME Larry himself introduced this assumption some years ago, but it was not there in 1998 when I introduced the name space concept in Isabelle. ML tools should not guess at the layout of full names. This is an abstract datatype that happens to be implemented as string for historical reasons. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Two problems
Hi all,
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
begin
nondeterministically gives either
*** Undeclared type constructor: vname (line 12 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
*** Failed to parse type
*** in type abbreviation fdecl
*** At command type_synonym (line 11 of
/Users/blanchet/afp/thys/Jinja/Common/Decl.thy)
or
*** Inner lexical error at: ⟪i:U⟫ ⊢ t : T ⟹
*** IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i]) (line 91 of
~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
*** Failed to parse proposition
*** At command lemma (line 90 of
~~/src/HOL/Proofs/Lambda/StrongNorm.thy)
but each of them loads fine on its own.
2. I then wanted to try in jEdit but isabelle jedit gives this error:
### Building Isabelle/jEdit ...
src/graphview_dockable.scala:45: error: object graphview is not a member of
package isabelle
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:45: error: too many arguments for constructor
Object: ()java.lang.Object
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:53: error: value peer is not a member of
AnyRef{def make_tooltip(parent: javax.swing.JComponent,x: Int,y: Int,body:
isabelle.XML.Body): String}
graphview.add(panel.peer, BorderLayout.CENTER)
^
three errors found
Failed to compile sources
From what I recall, isabelle jedit worked fine on my machine (Mac OS X 10.6)
just one or two weeks ago.
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Am 03.12.2012 um 22:31 schrieb Jasmin Christian Blanchette: I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP (40ecbad14077). 1. In Proof General: theory Scratch imports $MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe ~~/src/HOL/Proofs/Lambda/StrongNorm begin I investigated some more, and this problem is clearly related to the existence of two theories called Type.thy -- which one gets picked up depends on luck. So I guess that's a known issue. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson: Missing components maybe? I did isabelle components -a earlier today. In fact, the issue is likely to be related to the big upgrade that resulted from my invocation of this very command yesterday night. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Did you try starting jEdit with -f to force a fresh build? Jasmin Blanchette jasmin.blanche...@gmail.com schrieb: Am 03.12.2012 um 23:08 schrieb Lawrence Paulson: Missing components maybe? I did isabelle components -a earlier today. In fact, the issue is likely to be related to the big upgrade that resulted from my invocation of this very command yesterday night. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two problems
Am 04.12.2012 um 07:51 schrieb Lars Noschinski: Did you try starting jEdit with -f to force a fresh build? That did the trick. Thanks! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
