Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Hi all, On 19.08.2011 01:38, Gerwin Klein wrote: Should we ask a wider audience (isabelle-users) if anybody else has good reasons against/for a change? Another small advantage of set as an own datatype arises in the context of subtyping. We use map functions to lift coercions between base

[isabelle-dev] set_comprehension_pointfree simproc losing bounds

Hi all, the following produces a Loose bound variable with Isabelle/4a15873c4ec9 theory Scratch imports Main begin lemma finite {y |y. ∃x. y ∈ f x} apply simp oops end Fortunately, jedit treats a proof that used to work (but fails now due to the above) as a sorry, such that I can continue

Re: [isabelle-dev] push request (Sublist.thy)

The test run was ok, but the repository is corrupted once again. Trying to repair by stripping. Dmitriy On 13.12.2012 13:23, Dmitriy Traytel wrote: It worked for me. I'm currently building (or more precisely running the build tool ;-) ) and will push if it succeeds. Dmitriy On 13.12.2012

Re: [isabelle-dev] push request (Sublist.thy)

). Dmitriy On 13.12.2012 13:58, Dmitriy Traytel wrote: The test run was ok, but the repository is corrupted once again. Trying to repair by stripping. Dmitriy On 13.12.2012 13:23, Dmitriy Traytel wrote: It worked for me. I'm currently building (or more precisely running the build tool

Re: [isabelle-dev] push request (Sublist.thy)

On 17.12.2012 15:23, Makarius wrote: On Thu, 13 Dec 2012, Dmitriy Traytel wrote: I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached error log was generated. hg verify on the server says that c4a27ab89c9b is the first damaged changeset. The corrupted repository is still

Re: [isabelle-dev] Repository trouble

I'm looking intro it. Dmitriy On 21.12.2012 04:07, Christian Sternagel wrote: Dear all, just now, when I tried hg in in the development repo, I got the error below. My mercurial version is 2.2.3 (for at least some weeks). Did anybody else experience similar problems? cheers chris

Re: [isabelle-dev] Repository trouble

No one knows if somebody is doing something wrong. I did a fresh clone (from the topmost non corrupted changeset) once again. Few commits are missing (I think by Jasmin and Sascha), as I didn't have them locally. You are both welcome to repush through lxbroy10 (please avoid macbroy20-29).

Re: [isabelle-dev] Automated testing questions

Hi Clemens, On 17.03.2013 20:43, Clemens Ballarin wrote: 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? I do use

[isabelle-dev] Where are the error messages?

Hi, theory Scratch imports Main begin term True x thm TrueI[OF TrueI] end behaves very strangely in jedit with Isabelle/5dbe537087aa. For both commands there is no indication of errors (except of the absence of a popup). This seams to apply to all Isar commands involving

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

expressions to work with the new translation check phase? - Brian On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote: * Nested case expressions are now translated in a separate check phase rather than during parsing. The data for case combinators is separated from

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

changes to the handling of case expressions? - Brian On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote: * Nested case expressions are now translated in a separate check phase rather than during parsing. The data for case combinators is separated from the datatype

Re: [isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

On 24.04.2013 16:18, Brian Huffman wrote: On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote: However, your example is still not printed as expected (assuming that the output should be equal to the input in this case): (case x of (a, b) = λ(c, d). e) y Usually prod_case

[isabelle-dev] Global build failures of the AFP in the testboard

Hi all, since Containers are in the AFP mira results in global crashes of the build tool (http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694). By global I mean that no session is built at all due to an outdated (wrt Isabelle repository, e.g. 916271d52466)

Re: [isabelle-dev] Global build failures of the AFP in the testboard

Am 15.05.2013 15:48, schrieb Makarius: What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how everything works out. It is also possible to make a quick integrity check via isabelle

Re: [isabelle-dev] Global build failures of the AFP in the testboard

Am 15.05.2013 16:34, schrieb Makarius: On Wed, 15 May 2013, Dmitriy Traytel wrote: Am 15.05.2013 15:48, schrieb Makarius: What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how

Re: [isabelle-dev] type unification

Hi Chris, I think Variable.polymorphic is what you want to use before using fastype_of. Dmitriy Am 11.07.2013 05:12, schrieb Christian Sternagel: Dear list, what is the proper way of obtaining a type from a term, in case I want to give it as argument to Sign.typ_unify (of Sign.typ_match

Re: [isabelle-dev] type unification

, Dmitriy Traytel wrote: Hi Chris, I think Variable.polymorphic is what you want to use before using fastype_of. Dmitriy Am 11.07.2013 05:12, schrieb Christian Sternagel: Dear list, what is the proper way of obtaining a type from a term, in case I want to give it as argument to Sign.typ_unify

Re: [isabelle-dev] lemma addition

Am 25.07.2013 04:16, schrieb Christian Sternagel: Dear developers, While the following lemma is proved automatically lemma converse_subset: A¯ ⊆ B¯ ⟷ A ⊆ B by auto I'm not sure exactly how, since simp_trace shows no application of simplification rules and neither of the rules suggested

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

Am 04.08.2013 18:57, schrieb Florian Haftmann: For nonnested recursive datatypes, compatibility is quasi-100%; and for nested datatypes, the package will support an optional nested to mutual reduction to simulate the old package, so that the same theorems as before are available (albeit under

Re: [isabelle-dev] Sledgehammer proof text insertion

Am 05.09.2013 13:35, schrieb Florian Haftmann: I also observed that if you use sledgehammer as old-style keyword, the proof text is inserted after instead of just replacing lemma distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m sledgehammer by (metis distinct_conv_nth)

Re: [isabelle-dev] Isabelle2013-2 release

From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But I'm waiting for Christian to confirm this. Dmitriy Am 21.11.2013 00:13, schrieb René Neumann: If there will already be a new release, would it perhaps be possible to merge the fix (given there is a robust one) for this

[isabelle-dev] Outdated state after opening theories from images

This refers to Isabelle/d71c2737ee21. The minimal example is really minimal this time: theory Scratch imports Main begin end In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy is now outdated as well. The

Re: [isabelle-dev] Outdated state after opening theories from images

Am 22.11.2013 21:40, schrieb Makarius: On Fri, 22 Nov 2013, Dmitriy Traytel wrote: This refers to Isabelle/d71c2737ee21. The minimal example is really minimal this time: theory Scratch imports Main begin end In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a moment

Re: [isabelle-dev] AFP failures

Zorn is supposed to move to Main together with the new (co)datatype package. I guess it was removed from Library only by mistake. Dmitriy Am 26.11.2013 12:58, schrieb Lawrence Paulson: Of course we don’t have any formal curation policy for the library, but Zorn's lemma is a fundamental

Re: [isabelle-dev] text_fold

Am 10.02.2014 14:18, schrieb Makarius: On Mon, 25 Nov 2013, Dmitriy Traytel wrote: Am 23.11.2013 19:42, schrieb Makarius: On Mon, 28 Oct 2013, Dmitriy Traytel wrote: Concerning the error messages: at least you should always get strictly more information than without coercion inference

Re: [isabelle-dev] HOL-IMP very slow

Should be fine again (or at least better) with b445c39cc7e9. Thanks for the notification. Dmitriy Am 12.02.2014 16:28, schrieb Makarius: Tests about slowness take long, but here is a presumably good point in the published history: Isabelle/db691cc79289 Finished Pure (0:00:10 elapsed time,

Re: [isabelle-dev] HOL/Library/Code_Prolog.thy breakdown

Am 13.02.2014 12:48, schrieb Makarius: Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy. This was undetected in a more regular test due to this change that removed it from the normal HOL-Library session: changeset: 38504:76965c356d2a user:haftmann date:

Re: [isabelle-dev] NEWS: improved support for Isabelle/ML

Hi Makarius, Am 17.02.2014 14:14, schrieb Makarius: * Improved support for Isabelle/ML, with jEdit mode isabelle-ml for auxiliary ML files. This refers to Isabelle/56ebc4d4d008. It continues recent improvements of auxiliary file support. The IDE support for Isabelle/ML is already quite

Re: [isabelle-dev] set_comprehension_pointfree simproc

Am 14.03.2014 13:36, schrieb Makarius: What is the status of the set_comprehension_pointfree simproc? In 31afce809794 Dmitriy says set_comprehension_pointfree simproc causes to many surprises if enabled by default, and in 4d899933a51a I've tried to reconstruct the missing NEWS entry, since

Re: [isabelle-dev] NEWS: improved support for Isabelle/ML

Am 31.03.2014 23:14, schrieb Makarius: On Fri, 28 Feb 2014, Makarius wrote: I've made another round of refinements (presently at Isabelle/f7ceebe2f1b5). There were some situations where the change propagation of blobs (auxiliary files) versus theories was not right, leading to an invalid

Re: [isabelle-dev] status (AFP)

Could it be the document preparation? Dmitriy Am 05.05.2014 11:17, schrieb Johannes Hölzl: Has anybody an idea why the AFP test for Probabilistic_Noninterference fails? When I build it on my machine with either the combination in the email (i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or

Re: [isabelle-dev] bnf_decl axiomatization

Am 12.05.2014 16:54, schrieb Makarius: This is a continuation of the thread: code_pred introduces axioms? (October / November 2013). Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote: When Lukas told me about the axioms about three years ago, he said that indeed these axioms only

Re: [isabelle-dev] bnf_decl axiomatization

Am 13.05.2014 08:09, schrieb Jasmin Christian Blanchette: Am 12.05.2014 um 23:10 schrieb Makarius makar...@sketis.net: This sounds both a bit like testing-unstable-HOL. But there is no problem to experiment with axiomatizations, if it clear to the user what it is, and not a seamingly

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 11:07, schrieb Jasmin Blanchette: Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate constants: map_list vs. map set_list vs.

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 11:46, schrieb Tobias Nipkow: On 26/05/2014 11:07, Jasmin Blanchette wrote: Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de: The definition of list should look like before. I don't see how this is an option. This would result in the following duplicate

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 12:25, schrieb Makarius: On Sun, 25 May 2014, Jasmin Christian Blanchette wrote: The = as the name for Nil's discriminator deserves an explanation. [...] So I introduced this weird = syntax, which suggests that equality is used for discriminating. I am open to other suggestions.

Re: [isabelle-dev] Notes on datatype_new list

Am 26.05.2014 12:53, schrieb Makarius: On Mon, 26 May 2014, Dmitriy Traytel wrote: Just on the squiggles in isolation: if these are rare add-on options one could invent long / explicit keywords for them (or Parse.literal items). grep gives 371 occurences of -: in IsaFoR's development

[isabelle-dev] Fwd: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

on Derivatives of Regular Expressions Dmitriy Traytel and Tobias Nipkow Monadic second-order logic on finite words (MSO) is a decidable yet expressive logic into which many decision problems can be encoded. Since MSO formulas correspond to regular languages, equivalence of MSO formulas can be reduced

Re: [isabelle-dev] Problems with datatype-new

Hi René, this is a tactic failure in the recent size extension (the interface with fun). We will work on it. Thanks for the report, Dmitriy On 25.06.2014 13:49, René Thiemann wrote: Dear all, I have an unexpected problem when defining a datatype using datatype_new. theory Test imports

Re: [isabelle-dev] default cases rule

Hi Chris, Am 05.09.2014 um 12:27 schrieb Christian Sternagel: [...] First question: is this intentional and what is the current default rule? Yes. Quoting from the news: The rule set_cases is now registered with the [cases set] attribute. This can influence the behavior of the cases

Re: [isabelle-dev] Datatypes Isatest failures

On 17.09.2014 11:40, Jasmin Christian Blanchette wrote: There are only a handful of old_datatypes left in the AFP, and they will go away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back from vacation). It is now (isabelle/7b92932ffea5) fixed, and the

Re: [isabelle-dev] Problem in the AFP

Yes, that's my bad. Thanks! I was about to check Mira for complaints. See now AFP/ 1dd93cc85dfb. Dmitriy On 23.10.2014 14:25, Florian Haftmann wrote: Isabelle 06dfbfa4b3ea AFP 33c18a9138e9 *** Unknown old-style datatype Regular_Exp.rexp *** At command derive (line 18 of

Re: [isabelle-dev] HOL/Number_Theory/Primes

This is in Isabelle2014. In 229765cc3414 I make the same measurements as Larry. So indeed (as the text above those lemmas suggests) there seems to be a regression with the simplifier setup. Dmitriy On 07.11.2014 15:10, Julian Brunner wrote: The proof that 97 is prime only takes 1.3s on my

Re: [isabelle-dev] HOL/Number_Theory/Primes

hasty to remove the test which exposed this time leak. Once this issue has been fixed, I will put the long test back in, with a better comment. Tobias On 07/11/2014 15:27, Dmitriy Traytel wrote: This is in Isabelle2014. In 229765cc3414 I make the same measurements as Larry. So indeed

[isabelle-dev] HOL broken?

http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71 anybody taking care of this? Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] is_concealed

Sorry for reviving an ancient thread, but have the constants defined by inductive ever been visible to find_consts since Florian's commit (I presume 4a3747517552 ?). Today in be4a911aca71 (but also in Isabelle2014 and even in Isabelle2012) in the following inductive xyz :: bool where xyz

Re: [isabelle-dev] BNF: dead or alive?

-functions (and appropriately plug in ids in the internal BNF constructions)?. Let me cite the relevant part of my email that you refer to. On 13.11.2014 15:40, Dmitriy Traytel wrote: I would not care too much about such dead annotations. If a user made a variable dead explicitly, she might

Re: [isabelle-dev] BNF: dead or alive?

On 21.11.2014 15:00, Christian Sternagel wrote: Hi Dmitriy, thanks for another round of clarification (I should really reread old emails before referring to them). On 11/21/2014 02:43 PM, Dmitriy Traytel wrote: In general, why not create map-functions that allow to map over *all* type

Re: [isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

the changes to a test server, and push them to the main repo if everything is fine? cheers chris On 11/23/2014 11:42 AM, Dmitriy Traytel wrote: Hi Christian, just a few weeks ago, I learned that Envir.subst_term_types is indeed the wrong function when substituting with a unifier (instead

Re: [isabelle-dev] adhoc overloading: ugly output

Hi Chris, I've pushed it to the testboard (and will push it to the repository in case of success): http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac Cheers, Dmitriy On 28.01.2015 09:55, Christian Sternagel wrote: It is amazing how easy some things get when a wizard is looking

Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level

Hi Makarius, On 10.02.2015 18:30, Makarius wrote: On Tue, 4 Nov 2014, Makarius wrote: Strange hacks that work around the absence of proper options encumber the introduction of them eventually. It is the usual bootstrap problem for reforms. I actually did start some work in the vicinity of

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

:04, Dmitriy Traytel wrote: Hi Andreas, I've investigated this a bit and the slowdown happens in the code plugin in the instantiation of the equal type class (i.e. datatype (plugins del: code) is more precise than the advice below). The number of theorems proved there is quadratic (8000 in your

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

Hi Andreas, rather than going dirty, try: datatype (plugins only:) family ... It seems that here we are lucky and the slowdown is caused by one of the plugins. (We'll investigate which one.) Cheers, Dmitriy PS: Your datatype reminded me of another one, which allows (or allowed) proving

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

tactics. Cheers, Andreas On 09/04/15 15:55, Dmitriy Traytel wrote: Hi Andreas, rather than going dirty, try: datatype (plugins only:) family ... It seems that here we are lucky and the slowdown is caused by one of the plugins. (We'll investigate which one.) Cheers, Dmitriy PS: Your datatype

Re: [isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore

Hi Makarius, thanks, this is the hint I was looking for a long time now. I will do the replacement in the BNF package, but I don't think that I will have time for it before the approaching release. Dmitriy On 07.04.2015 17:47, Makarius wrote: Just a short note on Local_Theory.open_target

Re: [isabelle-dev] Remaining uses of defer_recdef?

Hi Florian, On 06.06.2015 17:11, Florian Haftmann wrote: The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple)

Re: [isabelle-dev] Remaining uses of defer_recdef?

Hi, I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). I'm not sure if

Re: [isabelle-dev] »real« considered harmful

I guess what Larry means is there is no way to see a type of a constant that is not there in the source. Consider e.g. declare [[coercion of_nat :: nat ⇒ real]] term sqrt (2 :: nat) Today the output says sqrt (real_of_nat 2). But if there would be no abbreviation for of_nat :: nat ⇒ real,

Re: [isabelle-dev] »real« considered harmful

You can hover in the output panel, but you won't see types of constants there. Dmitriy On 24.06.2015 16:09, Manuel Eberl wrote: Ah, I see the problem. In that case, one could still hover over the of_nat in the output window, but it is perhaps not ideal. On 24/06/15 16:08, Dmitriy Traytel

Re: [isabelle-dev] Fwd: isabelle test failed

Oops, I didn't expect my name to appear here ;-) The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. With turned off proofs the effect was a good one. What is special about Pure.conjunction w.r.t. proof reconstruction? Is it something in Goal.conjunction_tac? Would

Re: [isabelle-dev] testboard

On 19.08.2015 22:45, Makarius wrote: On Wed, 19 Aug 2015, Larry Paulson wrote: I pushed a changeset to the testboard, but it isn’t showing up at http://isabelle.in.tum.de/testboard/Isabelle The last change it shows was 6 days ago. Moreover, testboard and the default branch look identical

Re: [isabelle-dev] copy_bnf

Hi Lars, this was exactly the vision for copy_bnf, modulo that I thought of using a plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not the author of record, I went for the less invasive option of a separate command (in the spirit of setup_lifting for typedef). So if

Re: [isabelle-dev] Broken AFP sessions

Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is now a simprule). Verified only for the Integral.thy failure. Dmitriy > On 06 Oct 2015, at 23:19, Makarius wrote: > > Here are some more proof failures (Isabelle/5b5656a63bd6 and >

Re: [isabelle-dev] HOL-Proofs broken?

As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about 17 minutes. Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64 Dmitriy > On 06 Oct 2015, at 21:54, Jasmin Blanchette > wrote: > > Hi Makarius, > >> My

[isabelle-dev] Multiset missing Nitpick_Model.unrep in 2007ea8615a2

The title says it all. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Scrollbar, where are thou?

Hi, I’m not sure if this is rather something for the jEdit mailing list, but I try here first. The attached theory is an empty 500+ lines long file where everything is normal. However, if I add one new line the scrollbar disappears. The above applies to 2007ea8615a2 but I believe I saw this

Re: [isabelle-dev] NEWS

Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly, case_prod is the "right" name from the perspective

Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]

) = f« prints as »curry (λ(x, y). f x y) = f« by default. Any headache with this? Florian Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third

Re: [isabelle-dev] Update of jdk and jedit components

Hi Makarius, here is one way to still (e1e6bb36b27a) edit the output buffer: to use the compose key. On my Mac, if I place the cursor into the output buffer and press alt-u followed bei u, an ü appears in the output. Dmitriy > On 04 Nov 2015, at 20:42, Makarius wrote: >

Re: [isabelle-dev] Maintenance work on Jenkins VM

Hi Lars, great to hear! What about having an additional afp_testboard repository where one could also push -f changes. I am particularly interested in “slow” sessions there. Thanks for your work, Dmitriy > On 30 Jan 2016, at 12:51, Lars Hupel wrote: > > Dear list, > > I'm

Re: [isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)

Maybe a guess in the blue, but here is what grep tells me: ~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick /Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML: val name = Long_Name.base_name tyco I have not investigated further. Dmitriy > On 27 Feb 2016, at

Re: [isabelle-dev] Jenkins maintenance window

Hi Lars, I am unsure if an Isabelle tool is the right level of abstraction for an operation, only members of the isabelle (UNIX) group at TUM can/should execute. Also, wouldn’t a push to a fresh repository take quite long. (OK, negligible compared to the actual build, but still.) And one still

Re: [isabelle-dev] Jenkins maintenance window

> On 16 Feb 2016, at 11:30, Makarius <makar...@sketis.net> wrote: > > On Tue, 16 Feb 2016, Dmitriy Traytel wrote: > >> I am unsure if an Isabelle tool is the right level of abstraction for an >> operation, only members of the isabelle (UNIX) group at TUM ca

Re: [isabelle-dev] Maintenance work on Jenkins VM

Hi Lars, even without the slow sessions, this is of great help. Thanks! My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because without the afp_testboard, I used to follow the "break it, fix it” philosophy w.r.t. AFP). I will repair those today. Dmitriy > On 17 Feb 2016,

Re: [isabelle-dev] Jenkins updates

Hi Lars, thanks for your work. Unfortunately, currently pushing to testboard/isabelle does not seem to trigger new builds. Is this related to the job renamings? Another renaming issue is visible here: https://ci.isabelle.systems/status/ The status icon still points to (the now non-existent)

Re: [isabelle-dev] NEWS: Local_Theory.restore versus Local_Theory.reset

> On 05 Mar 2016, at 23:11, Makarius wrote: > > *** ML *** > > * Local_Theory.restore has been renamed to Local_Theory.reset to > emphasize its disruptive impact on the cumulative context, notably the > scope of 'private' or 'qualified' names. Note that Local_Theory.reset

[isabelle-dev] Discovering named_theorems

Hi all, trying the smaller audience of isabelle-dev first. I wondered whether named_theorems (or more generally all dynamic facts) deserve to be more visible. In particular when I search for "(?a < ?c - ?b) = (?a + ?b < ?c)” with find_theorems, I’d like to be reminded of algebra_simps

Re: [isabelle-dev] Discovering named_theorems

Hi Makarius, > On 10 May 2016, at 22:48, Makarius <makar...@sketis.net> wrote: > > On 03/03/16 14:19, Dmitriy Traytel wrote: > >> I wondered whether named_theorems (or more generally all dynamic facts) >> deserve to be more visible. In particular when I search

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

Hi Makarius, this is nice. At first I was a bit surprised to see the first occurrence of list, Nil, and Cons in blue in the following datatype definitions. datatype 'a list = Nil | Cons 'a "'a list” But I guess, it makes sense to indicate that this is a new thing being defined. The question

Re: [isabelle-dev] map/rel/set for lift_bnf

Hi Lars, thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f. Note that this still doesn’t provide the interface to Lifting and Transfer via transfer rules for the BNF constants (which is more complicated since lift_bnf doesn’t know about Lifting, in particular about the correspondence

Re: [isabelle-dev] Uses of Jenkins at TUM

Hi Makarius, > On 24 Apr 2017, at 18:12, Makarius wrote: > > On 24/04/17 14:46, Makarius wrote: >> >> Are there users of it outside the TUM group? My usage is the same as in Jasmin’s and Andreas’ case. >> >> What is good about it? What is bad about it? > > (1) To

Re: [isabelle-dev] the new "imports" semantics

Hi Larry, in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means that you must import it without any session qualification (just like Main or Complex_Main). Dmitriy > On 2 Nov 2017, at 17:47, Lawrence Paulson wrote: > > I’ve been converting some

Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

Hi all, thanks for pointing this out, Lars. And thanks for looking at the sources, Jasmin. The problem seems to only show up when the declaration in question is inside of a class context. Here is a reduced version that does not involve primrec at all. context linorder begin context fixes b

Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

Hi Makarius, > On 1 Jun 2018, at 23:32, Makarius wrote: > > On 01/06/18 10:35, Dmitriy Traytel wrote: >> Hi all, >> >> thanks for pointing this out, Lars. And thanks for looking at the sources, >> Jasmin. >> >> The problem seems to only show