Re: [isabelle-dev] Changes to the locale syntax
On Wed, 28 Oct 2015, Clemens Ballarin wrote:
I'm planning two moderate changes to the locale syntax:
* The default of qualifiers in locale expressions will change from
optional ("?") to mandatory ("!") in the context of "locale" and
"sublocale". This brings these commands in line with "interpretation"
and "interpret". In larger developments it is apparent that this is
the better default.
When we introduced that difference of defaults around 2007, it was based
on a vague intuition about the most common uses in typical application.
I don't mind to change that, and thus make it more uniform. It is mainly
a matter of the empirical situation found in the visible universe of
Isabelle examples + AFP if it is feasible / desirable.
* As already mentioned in my previous message, I plan to change the
keyword for rewrite morphisms from "where" to "rewrites". This is to
better distinguish these from named instantiations in locale
expressions. The syntax will then be
sublocale A < B where y = x for x rewrites "z = w"
rather than
sublocale A < B where y = x for x where "z = w"
Side remark: isabelle build -k helps to test hypotheses about feasibility
of new keywords. E.g.
isabelle build -d '$AFP' -k rewrites -n -a
No conflicts here.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Repository version of Isabelle on Windows 7
I am trying to install the repository version (f2e51e704a96) of Isabelle on Windows 7 using Cygwin by following README_REPOSITORY. Cygwin with Perl and Mercurial are installed, so I follow step 2 of README_REPOSITORY: Anders@r099121 /cygdrive/c/repo-isabelle $ uname -a CYGWIN_NT-6.1-WOW r099121 2.2.1(0.289/5/3) 2015-08-20 11:40 i686 Cygwin Anders@r099121 /cygdrive/c/repo-isabelle $ hg clone http://isabelle.in.tum.de/repos/isabelle destination directory: isabelle requesting all changes adding changesets adding manifests adding file changes added 61525 changesets with 165242 changes to 10175 files updating to branch default 3101 files updated, 0 files merged, 0 files removed, 0 files unresolved Anders@r099121 /cygdrive/c/repo-isabelle $ cd isabelle Anders@r099121 /cygdrive/c/repo-isabelle/isabelle $ hg id f2e51e704a96 tip Anders@r099121 /cygdrive/c/repo-isabelle/isabelle $ ./bin/isabelle components -I ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/csdp-6.x" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/cvc4-1.5pre-2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/e-1.8" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/exec_process-1.0.3" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/Haskabelle-2015" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/isabelle_fonts-20151021" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jdk-8u66" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jedit_build-20151023" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jfreechart-1.0.14-1" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jortho-1.0-2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/kodkodi-1.5.2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/polyml-5.5.3-20150916" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/scala-2.11.7" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/spass-3.8ds" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/xz-java-1.2-1" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/z3-4.4.0pre" User settings file already exists! Edit "/cygdrive/c/Users/Anders/.isabelle/etc/settings" manually and add the following line near its start: init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" Anders@r099121 /cygdrive/c/repo-isabelle/isabelle $ cat /cygdrive/c/Users/Anders/.isabelle/etc/settings init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" Anders@r099121 /cygdrive/c/repo-isabelle/isabelle $ ./bin/isabelle components -a ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/csdp-6.x" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/cvc4-1.5pre-2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/e-1.8" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/exec_process-1.0.3" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/Haskabelle-2015" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/isabelle_fonts-20151021" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jdk-8u66" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jedit_build-20151023" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jfreechart-1.0.14-1" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/jortho-1.0-2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/kodkodi-1.5.2" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/polyml-5.5.3-20150916" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/scala-2.11.7" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/spass-3.8ds" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/xz-java-1.2-1" ### Missing Isabelle component: "/cygdrive/c/Users/Anders/.isabelle/contrib/z3-4.4.0pre" Unpacking "/cygdrive/c/Users/Anders/.isabelle/contrib/csdp-6.x.tar.gz" tar: This does not look like a tar archive gzip: stdin: unexpected end of file tar: Child returned status 1 tar: Error is not recoverable: exiting now Anders@r099121 /cygdrive/c/repo-isabelle/isabelle $ You see that I get an error. Why does this happen and what can I do to solve the problem? Cheers and thanks, Anders Schlichtkrull ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Repository version of Isabelle on Windows 7
On Fri, 30 Oct 2015, Anders Schlichtkrull wrote: Unpacking "/cygdrive/c/Users/Anders/.isabelle/contrib/csdp-6.x.tar.gz" tar: This does not look like a tar archive gzip: stdin: unexpected end of file tar: Child returned status 1 tar: Error is not recoverable: exiting now You see that I get an error. Why does this happen and what can I do to solve the problem? Somehow the downloaded csdp-6.x.tar.gz came out as corrupted. Just delete that file and try "isabelle components -a" again. If the problem persists, you should look more closely at the content of /cygdrive/c/Users/Anders/.isabelle/contrib/ Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions
On Thu, 29 Oct 2015, Florian Haftmann wrote: I have not spend any thoughts whether there could be terminaton issues. Is there any argument beyond the absence of counterexamples that that can never happen? Standard batch build prints relatively few terms, so this is not yet significant as a test. The following change prints every intermediate Isar toplevel state. With that I get timeouts or interrupts due to out-of-memory situation in various sessions, e.g. HOL-Nominal-Examples or Jinja. I did not look what really happens. This is Isabelle/d05f3d86a758 and AFP/20f80d4c7850. Makarius# HG changeset patch # User wenzelm # Date 1446231391 -3600 # Fri Oct 30 19:56:31 2015 +0100 # Node ID 75fa4c345fc77dbd8b5621205ed620f484896b6d # Parent d05f3d86a758931d5cd379b9ec86b766eebb20da test diff -r d05f3d86a758 -r 75fa4c345fc7 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Oct 30 17:14:30 2015 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Oct 30 19:56:31 2015 +0100 @@ -585,6 +585,7 @@ val (st', opt_err) = Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st) (fn () => app int tr st) (); +val _ = writeln (string_of_state st'); val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
