Re: [isabelle-dev] jEdit import theories
I used a literal ~ and changing this to $HOME solved the problem, thanks! cheers chris PS: Is it just me or is Isabelle/jEdit really much faster than ProofGeneral/emacs when loading theories? (Maybe this is due to some other difference between Isabelle2011-1 and the repo version; I only use emacs if I have to stick to Isabelle2011-1.) On 03/21/2012 01:24 AM, Makarius wrote: On Tue, 20 Mar 2012, Christian Sternagel wrote: Hi there, I am using an environment variable in an import statement like imports $VAR/Theory.thy in batch-mode this works fine. However, in jEdit I get an error message indicating Missing theory (file ...) where the path in the error message shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
On Wed, 21 Mar 2012, Christian Sternagel wrote: Is it just me or is Isabelle/jEdit really much faster than ProofGeneral/emacs when loading theories? (Maybe this is due to some other difference between Isabelle2011-1 and the repo version; I only use emacs if I have to stick to Isabelle2011-1.) Ça depend, as the French like to say. Isabelle/jEdit in Isabelle2011-1 and repository versions until today (8e1b14bf0190) uses a uniform model to process buffer content, intermixed with potential user edits, with full document markup reports that eventually causes the Haribo effect in the sources. This is done in a reasonably fast way, but there are still situations where too many goal states are printed and thus the prover session gets overloaded. (E.g. in Hoare_Parallel or AFP/JinjaThreads.) In contrast, Proof General / Emacs is very slow in processing the current buffer (especially on Mac OS), but resolves imports via the batch-mode theory loader of Isabelle, which is presently faster than any other way of processing theories. (The same is used for isabelle usedir/make/makeall.) The general direction is to unify old-style batch loading with new-style document processing, such that it is both very fast and produces the full markup. It will also overcome occasional confusions about different behaviour of tools in different modes of theory processing. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
On Tue, 20 Mar 2012, Christian Sternagel wrote: Hi there, I am using an environment variable in an import statement like imports $VAR/Theory.thy in batch-mode this works fine. However, in jEdit I get an error message indicating Missing theory (file ...) where the path in the error message shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
