[isabelle-dev] NEWS: transitivity reasoner

2007-09-19 Thread Clemens Ballarin
* 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

[isabelle-dev] [isabelle] Simplification in locales

2008-07-04 Thread Clemens Ballarin
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] Isabelle colours on emacs

2008-07-08 Thread Clemens Ballarin
If you use emacs (not xemacs) with Isabelle and would like to get the familiar colours in theory files you were used to on xemacs: here's the required custiomisation command. Clemens --- (custom-set-faces ;; custom-set-faces was added by Custom. ;; If you edit it by hand, you could mess

[isabelle-dev] [Fwd: SourceForge.net CVS Migration and Downtime Announcement]

2008-09-30 Thread Clemens Ballarin
I wouldn't bother either. Actually, I don't see any real benefit for us, but then you are in a better position to judge. Clemens On 29 Sep 2008, at 23:46, Gerwin Klein wrote: While we're at it: what is the general feeling towards migrating the AFP to svn?

[isabelle-dev] includes

2008-10-15 Thread Clemens Ballarin
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] Duplications in AFP

2008-10-16 Thread Clemens Ballarin
[This message is mainly directed to the AFP programme committee.] The AFP contains clones and duplications of theory files and even entire directories between the entries. For example, I recently discovered that JinjaThreads/DFA is an identical copy of Jinja/DFA (see the diff below).

[isabelle-dev] NEWS

2008-10-30 Thread Clemens Ballarin
* 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] Branch in isabelle repository

2009-10-01 Thread Clemens Ballarin
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

2009-10-01 Thread Clemens Ballarin
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

2009-10-19 Thread Clemens Ballarin
* Thoroughly revised locales tutorial. New section on conditional interpretation.

Re: [isabelle-dev] Local Specification Mechanisms: Brief Experience Report

2010-12-17 Thread Clemens Ballarin
Quoting Tjark Weber webe...@in.tum.de: Well, roundup bound is developer jargon. Yes, but this is just because the roundup algorithm hasn't been documented anywhere. If you have a permutation of more than five parameters, you might need to increase the bound (but I consider this very

[isabelle-dev] JinjaThreads

2010-12-18 Thread Clemens Ballarin
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.

Re: [isabelle-dev] Isabelle release

2011-01-06 Thread Clemens Ballarin
I think a release date of January 2011 still justifies to call the release Isabelle2010. Why would we want to, though? I suppose Makarius suggested this to be able to call the release due at the end of the year 2011 rather than 2011-1. Not that it's that important (which makes it all the

[isabelle-dev] NEWS

2011-01-07 Thread Clemens Ballarin
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

Re: [isabelle-dev] Proof General 4.1pre

2011-01-13 Thread Clemens Ballarin
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

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

2011-01-23 Thread Clemens Ballarin
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] Context of a locale?

2011-05-23 Thread Clemens Ballarin
Hi John, There is Locale.init, which seems to be what you want. Clemens Quoting John Munroe mun...@gmail.com: Hello Does anyone know of a way to obtain the context of a given locale name? There doesn't seem to be an appropriate function for this in locale.ML. Any help will be appreciated.

[isabelle-dev] Poly/ML

2011-06-21 Thread Clemens Ballarin
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

[isabelle-dev] Sledgehammer

2011-06-24 Thread Clemens Ballarin
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

2011-06-24 Thread Clemens Ballarin
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

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-25 Thread Clemens Ballarin
Quoting Makarius makar...@sketis.net: In principle everything is possible, but one needs to try hard to minimize options and features. Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play

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

2012-04-13 Thread Clemens Ballarin
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).

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

2012-04-18 Thread Clemens Ballarin
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] Interpretation [was HOL/ex/Set_Algebras]

2012-04-19 Thread Clemens Ballarin
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] Locale interpretation with mixins

2012-05-06 Thread Clemens Ballarin
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 with definitions [was Locale interpretation with mixins]

2012-07-23 Thread Clemens Ballarin
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

[isabelle-dev] Unable to push to Isabelle reop

2012-08-15 Thread Clemens Ballarin
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] Unable to push to Isabelle reop

2012-08-16 Thread Clemens Ballarin
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

Re: [isabelle-dev] PLATFORMS

2012-08-17 Thread Clemens Ballarin
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] document_output vs. old document_dump/document_dump_mode

2012-08-29 Thread Clemens Ballarin
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] Interpretation with definitions [was Locale interpretation with mixins]

2012-09-08 Thread Clemens Ballarin
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

2012-09-08 Thread Clemens Ballarin
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] Order of sublocale declarations

2013-02-09 Thread Clemens Ballarin
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

[isabelle-dev] Automated testing questions

2013-03-17 Thread Clemens Ballarin
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] Interpretation in arbitrary targets.

2013-03-26 Thread Clemens Ballarin
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

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

2013-04-02 Thread Clemens Ballarin
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.

2013-04-07 Thread Clemens Ballarin
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.]

2013-04-07 Thread Clemens Ballarin
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.]

2013-04-07 Thread Clemens Ballarin
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.

2013-04-12 Thread Clemens Ballarin
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.

2013-04-17 Thread Clemens Ballarin
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.

2013-04-17 Thread Clemens 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 of modularity

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

2013-04-18 Thread Clemens Ballarin
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.

2013-04-18 Thread Clemens Ballarin
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.

2013-05-21 Thread Clemens Ballarin
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.

2013-05-22 Thread Clemens Ballarin
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

[isabelle-dev] Isar syntax regression

2013-06-04 Thread Clemens Ballarin
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

2013-06-04 Thread Clemens Ballarin
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] Shadowing of theorem names in locales

2013-06-11 Thread Clemens Ballarin
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] isabelle jedit -l HOL fails

2013-10-01 Thread Clemens Ballarin
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

2014-01-10 Thread Clemens Ballarin
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

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

2014-02-11 Thread Clemens Ballarin
...@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

2014-03-21 Thread Clemens Ballarin
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

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

2014-06-27 Thread Clemens Ballarin
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] Problem with type inference in locale expressions

2014-09-04 Thread Clemens Ballarin
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

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

2014-09-06 Thread Clemens Ballarin
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:

[isabelle-dev] Regression in the sublocale command

2015-02-12 Thread Clemens Ballarin
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] Regression in the sublocale command

2015-02-15 Thread Clemens Ballarin
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

2015-02-14 Thread Clemens Ballarin
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

2015-02-14 Thread Clemens Ballarin
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

2015-02-14 Thread Clemens Ballarin
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

Re: [isabelle-dev] Future of permanent_interpretation

2015-10-25 Thread Clemens Ballarin
Hi Florian, this proposal goes too far, of perhaps, not far enough. Let me explain. There is of course nothing wrong with providing new commands and enhancements for frequent use cases. However, I don't see a good reason why users should be forced to write 'permanent_interpretation' where

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

2015-10-27 Thread Clemens Ballarin
> 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

[isabelle-dev] Changes to the locale syntax

2015-10-28 Thread Clemens Ballarin
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

2015-10-28 Thread Clemens Ballarin
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] Future of permanent_interpretation

2015-11-09 Thread Clemens Ballarin
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

2015-11-04 Thread Clemens Ballarin
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

2015-11-04 Thread Clemens Ballarin
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

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

2015-11-04 Thread Clemens Ballarin
On 30 October, 2015 20:02 CET, Makarius wrote: > 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

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

2015-11-18 Thread Clemens Ballarin
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] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

2015-12-23 Thread Clemens Ballarin
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] Future of permanent_interpretation

2015-11-18 Thread Clemens Ballarin
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] Supported Poly/ML versions

2016-02-14 Thread Clemens Ballarin
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

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

2017-08-25 Thread Clemens Ballarin
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

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

2017-08-29 Thread Clemens Ballarin
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.

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

2017-09-01 Thread Clemens Ballarin
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

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

2017-09-01 Thread Clemens Ballarin
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

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

2018-01-14 Thread Clemens Ballarin
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

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

2018-03-05 Thread Clemens Ballarin
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

2018-03-03 Thread Clemens Ballarin
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: