Re: [isabelle-dev] find_theorems and type class axioms

I agree, we should do something about it. All relevant people on our side currently are pretty busy with a project deliverable for 1st Dec, but we should be able to give find_theorems some of the TLC it deserves after that. This may not be easy to solve - it probably is just how matching/unific

[isabelle-dev] Immediate completion does not work anymore

As of the following revision, immediate completion does not work anymore in Isabelle/JEdit: changeset: 61600:1ca11ddfcc70 user:wenzelm date:Sat Nov 07 16:05:28 2015 +0100 summary: clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1); From the di

Re: [isabelle-dev] Future of permanent_interpretation

Hi Clemens, thanks for your feedback. > I have seen that you use the term 'mixin definition' in NEWS and isar-ref. I'm not sure this is needed but if so it must be explained. This is part of the still ongoing struggle for consistent terminology. Concerning equations, the term »rewrite morphisms

Re: [isabelle-dev] Future of isatest/afptest

> Reckon you could make the status of the builds somehow public? Definitely! There are already two jobs public at our Jenkins server: As soon as I add more jobs, they (and their output) will appear there. Unfortunately the old scheme of sending mails to t

Re: [isabelle-dev] Future of isatest/afptest

On 19 Nov 2015, at 00:18, Lars Hupel wrote: > > […] Lars, that all sounds awesome. Reckon you could make the status of the builds somehow public? (Right now I don’t know whether my patch to ConcurrentGC works or not, because I only get failure emails and don’t know when a build is run. I know

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

On Thu, 19 Nov 2015, Lawrence Paulson wrote: Library directory get special treatment. But I forget what this special treatment consists of. A long time ago, there was a slightly odd implicit load path for theories, and src/HOL/Library was part of it by default. Thus it was possible to impor

Re: [isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

On Mi, 2015-11-18 at 15:26 +, Lawrence Paulson wrote: > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works? Pushed. See Isabelle-dev, changeset 2e89bc578935 -- Peter > > Larry > > > Begin forwarded

Re: [isabelle-dev] find_theorems and type class axioms

This particular issue has, in fact, annoyed me a great deal. I needed the ‘dist_norm’ lemma a lot lately and was never able to find it with ‘find_theorems’, which was very frustrating. I eventually found it by reading a proof that used it somewhere. I did not think much of it at the time, but

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

As I recall, the Library directory get special treatment. But I forget what this special treatment consists of. It might make sense to move this particular entry to Library. Larry > On 19 Nov 2015, at 09:46, Florian Haftmann > wrote: > > Hi all, > >>> These suggestions are worth a discussio

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

I am partly to blame. The changes involving the “real” function caused a lot of disruption. I needed a week to get all of Isabelle/HOL working again, and thought it a more practical option to tackle the AFP failures after they occurred. Most of them were only out of action for a day. Larry > O

Re: [isabelle-dev] find_theorems and type class axioms

I had no idea that sort constraints played any role in the finding of theorems, or why they should play a role. Whatever function they have in a search doesn’t prevent the very similar query dist norm "op=“ from picking up quite a few things. To my mind it’s quite unintuitive and maybe

Re: [isabelle-dev] popup in ce6320b9ef9b

> Here is a minimal example, but I am at loss to explain what is going on > here. The usual reason for a term being annotated twice is that it is (type) checked twice. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.

Re: [isabelle-dev] popup in ce6320b9ef9b

Here is a minimal example, but I am at loss to explain what is going on here. Florian Am 18.11.2015 um 10:03 schrieb Tobias Nipkow: > In more than one example of locale interpretations with "where f = g", > where g is a constant, if I hover over the g, the popup shows the type > of g twic

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

Currently heating my CPU with test-building the patch ... If everything goes fine, I will push it. -- Peter On Do, 2015-11-19 at 10:46 +0100, Florian Haftmann wrote: > Hi all, > > >> These suggestions are worth a discussion. Should we go ahead? Would > anybody like to apply this patch and tes

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

Hi all, >> These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works? > > I could do it, if nobody has objections. I see no obstacles in going ahead. What requires some thought is the material in ex/ directories is

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

Hi Florian, > What is the reason for this? No access to suitable computing machines? currently, the "new" testboard only performs "makeall" on the distribution. As I wrote in my mail from yesterday, I'm working on it. I expect to be able to make a recommendation on how to reinstate regular testi

Re: [isabelle-dev] find_theorems and type class axioms

Hi Larry and Florian, the sort constraints for open, dist, and norm are changed in http://isabelle.in.tum.de/repos/isabelle/file/e89cfc004f18/src/HOL/Real_Vector_Spaces.thy#l1218 These constraints were introduced by Brian Huffman in 2d91b2416de8 while he was reworking the type class hierarchy

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

Thanks to all who have invested time and energy to work on those issues. Nevertheless I have the impression that in the last time there have have been lots of movements in the distribution being speculative in the sense that no systematic testing including the AFP had taken place. What is the rea

Re: [isabelle-dev] find_theorems and type class axioms

Hi Larry, > Andreas’s message reminds me that axioms of type classes are still not picked up: > > class dist_norm = dist + norm + minus + > assumes dist_norm: "dist x y = norm (x - y)” > > This item has the status of a theorem. However, the query > > dist "norm(_-_)” > > doesn’t find it. S