[isabelle-dev] NEWS: Locale rewrite morphism moved into expressions

In addition to Makarius' recent performance improvements, there is a modest reform to the way rewrite morphism are integrated with locales. Previously they were added as an after-thought to the interpretation commands. Now they are integrated with locale expressions. The main advantage is

[isabelle-dev] Deadlock while building HOL-Proof

While building HOL-Proof I observe a deadlock, usually after 13 min CPU time. It can be worked around with ISABELLE_BUILD_OPTIONS="threads=1". The deadlock occurs most of the time. The earliest changeset I was able to reproduce this with is changeset: 67675:738f170f43ee user:

[isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

Dear Maintainers of Isabelle / the AFP, Where would I find instructions on actually getting 'isabelle afp_build -A' to run through? I was hoping to find that in /doc/regression-test.md but that merely states the command. It appears that I would need to set ML_PLATFORM=x86_64-darwin for the

Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

On 2017-08-24 09:38, Thiemann, Rene wrote: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. Unless I hear otherwise I will replace \mu by LFP and \nu by

Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

On 2017-08-31 13:54, Florian Haftmann wrote: The theorem in question requires both the notion of subgroup and complete lattices, hence the import order dictates in which theory the theorem has to reside (btw. the current import order is similar to HOL-Main where Complete_Lattices comes after

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

On 2017-08-24 09:38, Thiemann, Rene wrote: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

Dear Florian, For the final record: Concerning \mu and \nu, I am currently investigating whether an import swap could re-establish the situation known from Isabelle2016-1 see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1 I had overlooked that \mu and \nu are global constants

Re: [isabelle-dev] Supported Poly/ML versions

On 13 February, 2016 16:22 CET, Makarius wrote: > > IMHO this sounds too obscure to be useful. How many users are actually > > aware of that possibility? > > Maybe 2-3 people on this mailing list, but this is only a guess. So lets > make a constructive proof and count

Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

Hi Florian, I didn't have time to look at your patches, and since I only have superficial knowledge of instantiation contexts I didn't fully understand the example either. I guess though that the purpose of these global interpretations is to propagate some constant declarations into the

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

I have now committed this. See isabelle/e89cfc004f18; the AFP didn't require changes. The final version does not activate abbreviations as aggressively as my first proposal. This was necessary so abbreviations are not propagated over rewrite morphisms, which would have been very confusing.

Re: [isabelle-dev] Future of permanent_interpretation

Hi Florian, I looked at the documentation generated with this patch, and the first impression of the "Locale interpretation" section is that it now looks funny -- probably due to the transitional nature of the patch. For "interpretation" there are now two declarations and two productions,

Re: [isabelle-dev] Future of permanent_interpretation

On 09 November, 2015 11:56 CET, Makarius wrote: > It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure > as separate command. If there is a simple way to have just one > 'interpretation' command with 'defines' vs. 'rewrites', I would prefer >

Re: [isabelle-dev] Changes to the locale syntax

I have now committed these changes. Clemens On 28 October, 2015 21:53 CET, "Clemens Ballarin" <balla...@in.tum.de> wrote: > I'm planning two moderate changes to the locale syntax: > > * The default of qualifiers in locale expressions will change from optio

Re: [isabelle-dev] Future of permanent_interpretation

Hi Florian, thanks for your feedback. Local theories have done Isabelle and its users a great service in presenting a uniform view of different kinds of declarations in several contexts, and the locales reimplementation would have been much more painful without them. However, if "local

[isabelle-dev] Changes to the locale syntax

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

Re: [isabelle-dev] Future of permanent_interpretation

ould also be kept in mind that "sublocale" is established in the locale documentation including my JAR paper [1]. If the desire for a different keyword is so strong, perhaps an alias might be a solution. Clemens [1] Clemens Ballarin. Locales: a module system for mathematical theories. Jour

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

> Since 'test' only depends on the parameter f, which is interpreted under > > the identity > > morphism (eta contraction seems to matter here, so this does not happen > > with your original > > example), all of these abbreviations are set up to be contracted be

Re: [isabelle-dev] Regression in the sublocale command

My conclusion of this discussion is that with 8fab871a2a6f the sublocale command immediately visits its target after the qed, which it didn't before. This now causes the command to loop. Is this correct? Clemens ___ isabelle-dev mailing list

Re: [isabelle-dev] Regression in the sublocale command

On 14 February, 2015 10:11 CET, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: I guess you found out using bisection. But I read some incertainty in your words »appears to have been introduced«. Is the changeset 8fab871a2a6f a reliable entrance point or a first

Re: [isabelle-dev] Regression in the sublocale command

to contrieve an example. Unfortunately, the looping is not reproducible in c3ca292c1484. Can you provide more detail? Thanks, Florian Am 12.02.2015 um 22:19 schrieb Clemens Ballarin: Hi Florian, I'm investigating a regression which prevents identifying certain equivalent locales

Re: [isabelle-dev] Regression in the sublocale command

This might indicate that something is wrong in the local theory stack here, maybe the last line in fun locale_dependency locale dep_morph mixin export = (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export # Locale.activate_fragment_nonbrittle

[isabelle-dev] Regression in the sublocale command

Hi Florian, I'm investigating a regression which prevents identifying certain equivalent locales through circular sublocale declarations: sublocale loc1 x: loc2 A c (* sigma_1 *) where x.b == B and x.d == e (* tau_1 *) sorry sublocale loc2 x: loc1 A b (* sigma_2 *) where x.c ==

Re: [isabelle-dev] Problem with type inference in locale expressions

This is what I expected. Type inference of locale expressions is inherently heuristic and probably you are hitting this. (This could be verified further with a stack trace). For more background, see also this earlier message:

Re: [isabelle-dev] Problem with type inference in locale expressions

Is this a regression in the type inference of locale expressions, or has it always (i.e. since 2009) been like this? Clemens On 04 September, 2014 09:21 CEST, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: At d6a2e3567f95, I am currently analysing a problem with type

[isabelle-dev] Isabelle/jedit reports that file was changed on disk

I occasionally get a modal dialog reporting that a the file I currently edit was changed on disk by another program and therefore automatically reloaded. I didn't touch or modify the program myself, and ls -l does not indicate a recent modification either. This is for a fairly recent

Re: [isabelle-dev] Shadowing of theorem names in locales

On 21 March, 2014 17:26 CET, Makarius makar...@sketis.net wrote: On Tue, 11 Feb 2014, Clemens Ballarin wrote: For the processing of locale expression, facts are not really required. Having all information related to syntax should be sufficient. I cannot tell, though, whether facts

Re: [isabelle-dev] Shadowing of theorem names in locales

...@sketis.net wrote: On Fri, 10 Jan 2014, Clemens Ballarin wrote: This does not exhibit itself until the compromised locale context is (re-)entered, and I think this is not desirable. My first spontaneous thought is that strictness should not apply during the initialisation of a locale

Re: [isabelle-dev] Shadowing of theorem names in locales

On 28 December, 2013 19:53 CET, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: HOL-Complex now builds with strict naming policy for facts (again). Thanks, that's cool. I have stumbled over something which needs some consideration: with strict naming policy, locales can

[isabelle-dev] isabelle jedit -l HOL fails

After updating the repository today (and a seemingly good run of 'isabelle components -a') 'isabelle jedit -l HOL' gives me 2013-10-01 20:42:22.345 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement methodSignatureForSelector: --

Re: [isabelle-dev] Shadowing of theorem names in locales

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: If you point we to particular occurences, I am willing to polish them accordingly. There are several versions of bounded_iff in the locales of that theory (and lattice locales from imported theories). To find all

[isabelle-dev] Isar syntax regression

I wonder whether then interpret Min!: semilattice_order_set min less_eq less. (without a space before the dot) is now intended Isar syntax. I found this in src/HOL/Big_Operators.thy, so I guess this is accepted in batch mode. PG doesn't accept it, but apparently JEdit does. Clemens

Re: [isabelle-dev] Shadowing of theorem names in locales

I recently tried to make HOL-Algebra compliant to this, but unfortunately got stuck in HOL already, where Big_Operators didn't comply either (but that's unlikely the only theory). If we are serious about forbidding duplicate theorem names eventually we probably need to start by introducing

Re: [isabelle-dev] Interpretation in arbitrary targets.

Quoting Lars Noschinski nosch...@in.tum.de: How is interpretation related to print_context? It seems that neither interpret nor interpretation extends the context as displayed by print_context? I don't know the answer to that, but for a particular locale x you should be able to find all

Re: [isabelle-dev] Interpretation in arbitrary targets.

Quoting Makarius makar...@sketis.net: Does it mean you propose to discontinue (in a) at some point? Exactly. Too early right now, but eventually this might make sense -- especially if the IDE provides suitable refactorings. Of course, this wouldn't let us scrap a lot of code, but the

Re: [isabelle-dev] Interpretation in arbitrary targets.

Hi Florian, OK, then we agree on this. Please let me know if you need to make changes to locales.ML. I want to make sure that routes out of certain quirks there don't get blocked accidentally. Clemens Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Hi Clemens,

Re: [isabelle-dev] Interpretation in arbitrary targets.

Ballarin: Quoting Makarius makar...@sketis.net: On Fri, 12 Apr 2013, Clemens Ballarin wrote: That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter

Re: [isabelle-dev] Interpretation in arbitrary targets.

Hi Florian, I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. This is fine with me. Will this work for

Re: [isabelle-dev] Interpretation in arbitrary targets.

Quoting Makarius makar...@sketis.net: On Fri, 12 Apr 2013, Clemens Ballarin wrote: That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter of modularity

Re: [isabelle-dev] Interpretation in arbitrary targets.

Hi Florian, I do not object to your suggestion, and it is clearly in reach within the current code base. But... it is a different thing. Your suggestion is to make sublocale work in locale targets seamlessly. But something like instantiation ... begin sublocale ... instance ... end then

Re: [isabelle-dev] Interpretation in arbitrary targets.

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. You have proposed a change about which doubts were raised. I don't consider it acceptable to

Re: [isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: context B begin context begin interpretation A end end This looks attractive, but could you please elaborate the semantics: - What would be the effect of the interpretation from the inner block on the outer

Re: [isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

Quoting Makarius makar...@sketis.net: On Tue, 26 Mar 2013, Florian Haftmann wrote: Note that we have one more aspect in the back-end that could help here: the 'private' modifier. What would the 'private' modifier do in general? This sounds like a new concept. The following may or may

Re: [isabelle-dev] Interpretation in arbitrary targets.

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. Well, here is my veto. I don't see that much of a discussion has taken place yet, and I am very

Re: [isabelle-dev] Interpretation in arbitrary targets.

Hi Florian, I'm in favour of generalising interpretation to targets, but in my opinion it would not be right to provide the sublocale command as the interpretation command in a locale context. There are two reasons: 1. sublocale modifies the locale graph of the underlying theory. This

[isabelle-dev] Automated testing questions

Dear Developers, What it the current best practice for testing my change to Isabelle? There used to be testboard, but I'm unsure how that evolved. Is there a similar service for testing my change to Isabelle against the AFP? Also, which server should I use for pushing my changes to

Re: [isabelle-dev] Order of sublocale declarations

Hi Andreas, The failure happens while reading the locale expression, which is a sequence of locale instances: A s + B t + C u + ... When reading the locale expression, we aim at achieving two conflicting goals: - Type inference over the entire expression - Syntax declarations of an

Re: [isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

Hi Florian, Anyway, I am not so much concerned about syntax. My primary intention is to get rid of the experimental code in interpretation_with_defs.ML, according to the following agenda: a) Decide for a particular syntax (at the moment this can only be (*) as it is conservative) b) Enhance

Re: [isabelle-dev] Locale interpretation with mixins

Quoting Makarius makar...@sketis.net: It means that a constant c that depends on context parameters x y z is turned into a fountational constant loc.c in the background, and then re-imported into the local context as loc.c x y z. Later it might get re-interpreted such that its dependency

Re: [isabelle-dev] document_output vs. old document_dump/document_dump_mode

For my most recent locales paper some tex files are generated with Isabelle 2009-1 because it uses the old axclass interface. The rest is produced with a current repository version. All files are dumped to the same document folder. I wonder whether there is any chance to convert this

Re: [isabelle-dev] PLATFORMS

Any chance of still working on Leopard if I neither use jEdit nor any of the external provers? Clemens Quoting Makarius makar...@sketis.net: Isabelle/10584ca5785f has an updated version of Admin/PLATFORMS. Executive summary: * Mac OS Mountain Lion is now supported (macbroy30) * Mac

Re: [isabelle-dev] Unable to push to Isabelle reop

Macbroy20 works for me. Thanks, Florian and Alex. Clemens Quoting Alexander Krauss kra...@in.tum.de: Quoting Clemens Ballarin balla...@in.tum.de: [...] pushing to ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle searching for changes remote

[isabelle-dev] Unable to push to Isabelle reop

I'm recently getting clemens-ballarins-macbook-air:IsarRef ballarin$ hg push Password: remote: Not trusting file /home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user wenzelm, group isabelle pushing to

Re: [isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

Hi Florian, I appreciate that you now follow my reasoning that changes to the locales core machinery are not necessary for getting this functionality. However, I don't think we should change how locale expressions work. Currently we have: locale loc = fixes x assumes about_x: x = x

Re: [isabelle-dev] Locale interpretation with mixins

Hi Florian, What is called mixin in the implementation is a transfer principle that is applied in addition to the interpretation morphism. Currently users can only give equations, which yield rewrite morphisms, and consequently, the term 'mixin' appears nowhere in the documentation. On

Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]

Hi Florian, I understood that much. What I was hoping for was an answer on a more technical level. The definition + interpretation pattern seem a useful thing to have. But it sounds like, if you change the main interpretation command like this, you will break it for intended use cases

Re: [isabelle-dev] HOL/ex/Set_Algebras

Hi Florian, Thanks for the clarification. Its purpose might have been to make the interpretation notationally simpler. the story behind is not about syntax. It is really about the simultaneous definitions. For a motivation, you can have a look at the tutorial on code generation, section

Re: [isabelle-dev] HOL/ex/Set_Algebras

I wondered when somebody would ask this. What's going on here is a hack, and I'm not very happy about it. If you follow up the imported theory, you will find some code that provides a clone of the interpretation command (under the same name!) with some added functionality (definitions).

[isabelle-dev] Sledgehammer

While doing an 'isabelle makeall all' on my local machine, I encountered the error Sledgehammering... *** Unexpected outcome: unknown. *** At command sledgehammer (line 26 of /Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy) I guess I lack some sort of heavy equipment

Re: [isabelle-dev] Sledgehammer

Hi Jasmin, Thanks for this hint. It turns out that I had set E_HOME to some bogus location. Residue of some old setup... Now it work fine. Clemens Quoting Jasmin Christian Blanchette jasmin.blanche...@gmail.com: Am 24.06.2011 um 20:13 schrieb Clemens Ballarin: While doing

[isabelle-dev] Poly/ML

After updating my Isabelle repository (which I haven't done for quite a while) Poly/ML stopped to start up. I have 5.2 and according to the release notes this is no longer supported. Do I need to build 5.4 for myself or do we provide a pre-built version for MacOS 10.5 somewhere? The

Re: [isabelle-dev] Proof General 4.1 on Mac OS X

I repeated my recent try of ProofGeneral on my Mac with ProofGeneral-4.1pre110118. If used with Aquamacs I observe these issues: - Menus respond slowly ( 1 second) when invoked for the first time. This is fine if Aquamacs is used without ProofGeneral. - Noise on the background shell.

Re: [isabelle-dev] Proof General 4.1pre

Quoting Makarius makar...@sketis.net: Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? I do. I recently tried to use PG 4.0 with Aquamacs 2.1. That didn't seem to work, so I went back to PG 3.7.1.1 and Carbon Emacs 1.6 (based on GNU Emacs

[isabelle-dev] NEWS

The upcoming release (which I guess will be called Isabelle 2011-0 Dispensable Debate) will have the following notable extensions to locale interpretation: * Locale interpretation commands 'interpret' and 'sublocale' accept lists of equations to map definitions in a locale to appropriate

[isabelle-dev] JinjaThreads

JinjaThreads doesn't seem to run out of the box (on macbroy2, with Poly/ML 5.3.0). It seems to run out of memory. I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately. Probably this is a known issue, but I don't know where to check for the automatic AFP logs.

[isabelle-dev] NEWS

* Thoroughly revised locales tutorial. New section on conditional interpretation.

[isabelle-dev] Branch in isabelle repository

Hi all, I wonder whether the second branch in the repository is intentional. See http://isabelle.in.tum.de/repos/isabelle/graph/a0f38d8d633a Unfortunately, it means that my revised locales code is now hidden from tip :-( Clemens

[isabelle-dev] Branch in isabelle repository

Actually, having a closer look at the actual graph, this is a false alarm. The the visualisation on that web page is misleading if not wrong. Clemens Quoting Clemens Ballarin ballarin at in.tum.de: Hi all, I wonder whether the second branch in the repository is intentional. See

[isabelle-dev] NEWS

* Dropped locale element includes. This is a major INCOMPATIBILITY. In existing theorem specifications replace the includes element by the respective context elements of the included locale, omitting those that are already present in the theorem specification. Multiple assume elements of a

[isabelle-dev] includes

Dear all, I'm planning a major revision of the locale implementation and consider removing includes altogether. Please get in touch if you have an application (outside the repository and afp) that depends on includes in a critical way. Clemens

[isabelle-dev] [isabelle] Simplification in locales

Currently not. Internally, a locale happens to be an interpretation in its decendants. But note that you could add [cong del] to any interpretations you make. Clemens On 3 Jul 2008, at 23:32, John Matthews wrote: Is there a way to only apply a theorem attribute inside a locale and its

[isabelle-dev] NEWS: transitivity reasoner

* The transitivity reasoner for partial and linear orders is set up for locales `order' and `linorder' generated by the new class package. Previously the reasoner was only set up for axiomatic type classes. Instances of the reasoner are available in all contexts importing or interpreting