Re: [isabelle-dev] Testing the QuickCheck setup

Dear Lars, Testing quickcheck is indeed quite tricky. Do you know which of the quickcheck calls time out? Does it happen only with the random generator or also with exhaustive? It might be that you have a fairly large set of code equations and the timeout already kicks in during code

Re: [isabelle-dev] NEWS: op -> ()

On 16/01/18 16:14, Lawrence Paulson wrote: On 16 Jan 2018, at 14:13, Blanchette, J.C. wrote: However, for operators like ==>, which bind on the right, foo ==> bar is actually much more readable than foo ==> bar This sort of claim needs

Re: [isabelle-dev] Slow builds due to excessive heap images

Hi Makarius, On 08/11/17 14:13, Makarius wrote: On 08/11/17 12:35, Tobias Nipkow wrote: On 07/11/2017 23:13, Makarius wrote: For Flyspeck-Tame a small performance loss remains. It might be worth trying to configure the Isabelle/HOL codegen to use FixedInt instead of regular (unbounded) Int.

[isabelle-dev] PolyML update

Dear list, I've been playing around with adding unsigned 64 bit integers to the AFP entry Native_Word. In doing so, I realised that PolyML in 64 bit mode has a bug in the Word64 implementation in the version that the current development version 2a6371fb31f0 uses (PolyML 5.6-1). For example,

Re: [isabelle-dev] Towards a "localized" code generator

Dear Lars, Well, we here at ETH have another function transformer, which can also be activated and deactivated basically with almost the same pattern. The only difference is that at the moment we use a command rather than a Config value because de- and reactivation in our case has to do a bit

Re: [isabelle-dev] Towards a "localized" code generator

Dear Lars, On 24/07/17 15:08, Lars Hupel wrote: 1) Function transformers: I want to run a function transformer in special situations. But I can only register it globally (with "Code_Preproc.add_functrans"). What I use is the following pattern: val enabled = Attrib.setup_config_bool @{binding

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

See now Isabelle/4c999b5d78e2. Andreas On 30/06/17 21:31, Tobias Nipkow wrote: On 30/06/2017 20:41, Manuel Eberl wrote: By the way, I recently encountered a similar (and even more nasty) name clash, with compact. The following works perfectly It's "Topological_Spaces.compact" and that

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

Hi all, Yes, it absolutely makes sense to change the situation with compact. It is a standard notion in order theory, so my suggestion is to make it qualified with ccpo, just like admissible and fixp are. I can take care of that. Andreas On 30/06/17 21:31, Tobias Nipkow wrote: On

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

. If anybody has better suggestions, I am open to implementing them. Manuel On 2017-06-28 17:05, Andreas Lochbihler wrote: Dear all, While porting some of my theories to the current development version, I've just noticed that the renaming of sublisteq to subseq done by Manuel in May

Re: [isabelle-dev] Efficient code for Discrete.log

Hi Manuel, You are not the first to encouter this problem. Here's my experience: In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile, Gcd has become part of Main again.

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

Dear all, While porting some of my theories to the current development version, I've just noticed that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad effect: The name subseq is already used in Topological_Spaces to formalise the concept of a

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

Sure. Whenever I have to push something to the Isabelle repository, I use the Jenkins testboard installation to see whether something broke. It works more reliably than the previous testboard infrastructure, which often ignored some commits. Andreas On 24/04/17 14:46, Makarius wrote: This is

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

Hi Florian, Lukas may be able to answer this question better, but here's a comment: You do not need the lazy treatment of irrefutable patterns in Haskell as a primitive, because it is easy to emulate using selectors. That is, if we have a single-constructor HOL datatype dataype 'a T = C (s1:

Re: [isabelle-dev] [isabelle] print_statement does not quote variables with reserved names

On 28/10/16 17:03, Makarius wrote: BTW, there is strictly speaking no need to use fix/assume/show, since show if/for is already possible, although relatively rarely used. I use show/if/for regularly in my work (just look at the AFP entry MFMC_Countable to see a few examples), but

Re: [isabelle-dev] Of lazy lists and friendly corecs

Hi Manuel, I've played around a bit with lmerge. It magically works if you replace the selectors with case statements (in Isabelle/5c2c559f01eb): friend_of_corec lmerge :: "int llist ⇒ int llist ⇒ int llist" where "lmerge xs ys = (case xs of LNil ⇒ (case ys of LNil ⇒ LNil | LCons y ys' ⇒

Re: [isabelle-dev] Of lazy lists and friendly corecs

Hi Manuel, a function is friendly if it produces at least one constructor after applying at most one constructor to the codatatype argument. This does not have anything to do with primitive corecursion, because the codatatype result type need not be a argument type---and even if it is, there

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

quot;finite" that does Code.abort in cases where finiteness wasn't obvious (e.g. complement), but I abandoned that idea for some reason. Still, at the moment, I think that might be the best solution. Any thoughts? Manuel On 03/10/16 17:37, Andreas Lochbihler wrote: Hi Manuel, Indeed, generic

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

nd returns "Code.abort … (f A)" for anything else (e.g. a set represented by the "coset" constructor). I planned on implementing this at some point, but I've quite a bit of other stuff to do and I wanted to discuss it first, so I never really got around to doing it. Cheers,

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

Hi René and Manuel, Indeed, for sets, expressing the code equations in terms of a generic iteration operation on sets would do the job for most of the cases. The comp_fun_commute and comp_fun_idem types in Containers precisely do this, but they have not been integrated in the HOL library

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

Hi Johannes, You could define the syntax for has_integral to be literally "(f Bochner.has_integral x) s" and similarly for the other. Additionally, you could declare bundles with the existing notation "(f has_integral x) s" for both of them (like is nowadays done for the Lifting

Re: [isabelle-dev] NEWS: proof outline with cases

Hi Makarius, Just a quick feedback on the proof outlines: they are great! But sometimes quotes are needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is a case of an induction rule by the function package for an equation which has been split up by the

Re: [isabelle-dev] Build NEWS

For published versions, there probably should not be any /devel-entries links. But for papers under submission, people may have updated their AFP entries and want the reviewers to access the updated material. At least that is what I used to do for many ITP submissions. So it might be good to

Re: [isabelle-dev] lifting syntax with proper symbols

Hi Makarius, How about LaTeX \Mapsto for ===>? This is what I use in my papers following Ondrej and Brian's paper on lifting. I'd be happy to have syntax for ===> enabled by default, as it makes transfer and parametricity rules much easier to read. I have no opinion on --->. Andreas On

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

Native_Word should work again in 203deaf5208d (see also 61aeecc4093d), both with GHC 7.8 and GHC 7.10. Andreas On 01/02/16 08:32, Andreas Lochbihler wrote: Hi Lars, The theory Uint comes from Native_Word. I'll have a look and see whether this can be fixed. Andreas On 31/01/16 22:21, Lars

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

Hi Lars, The theory Uint comes from Native_Word. I'll have a look and see whether this can be fixed. Andreas On 31/01/16 22:21, Lars Hupel wrote: * archival of the build logs As a temporary solution, I have now configured Jenkins to retain all build logs. I've found some pointers how to

Re: [isabelle-dev] AFP status

Applicative_Lifting and Stern_Brocot now (AFP/1c0036f62a32) work with Isabelle/adcaaf6c9910. Andreas On 13/01/16 00:06, Makarius wrote: The AFP status is much better than last week, but these sessions are still broken (Isabelle/7355fd313cf8 and AFP/87337b54f3eb): Applicative_Lifting

Re: [isabelle-dev] HOL-Codegenerator_Test error

Dear Manuel, I have not tried this explicitly, but it looks like the standard problem with type classes in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code equations use two type classes with an operation inherited from the same anchestor. The error

Re: [isabelle-dev] Problem with code generation for non-executable types

Hi Johannes, Then the dictionary construction for type constructors does not work in ML! The type signature would be the following: val test_prod : ('a * 'b) filter Which apparently is not allow in ML. This is the famous value restriction (which I also regularly run

Re: [isabelle-dev] CoreC++ broken

I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know what exactly went wrong or what caused the failure. The problem seems to be related to some change in theory imports. It seems as if code_pred cannot retrieve the specification of a constant under certain

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

Hi Larry, Type inferences assigns to "dist" the type "'a => 'a => real" where 'a :: metric_space, and to "norm" the type "'b => real" where 'b :: real_normed_vector (due to the type constraint manipulations in Real_Vector_Spaces.thy. The theorem dist_norm uses dist and norm with the sort

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

MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016. Presburger-Automata had a looping

Re: [isabelle-dev] NEWS

Dear Ondrej, Thanks a lot for this. Now I can scrap my own semi-working debugging infrastructure for transfer(_prover). Just a comments: Can you add a flag to transfer_step such that it outputs the rule it used as tracing information? My problem is that with big terms, I get a lot of

Re: [isabelle-dev] NEWS: 'consider' command and "cases" method

Dear Manuel, consider supports the same syntax as obtains, i.e., you can use "where" as in consider "x = ∞" | "x = -∞" | y where "x = ereal y" Andreas On 23/09/15 08:41, Manuel Eberl wrote: Is there a way to use ‘consider’ with fixed variables? E.g. if I have a rule like ereal_cases:

Re: [isabelle-dev] JinjaThreads

Hi Makarius, This might be due to my attempt to repair Predicate_Compile_Examples in 78ece168f5b5. I'll see what I can do. Andreas On 15/09/15 16:41, Makarius wrote: This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9: *** Failed to load theory "Execute_Main" (unresolved

Re: [isabelle-dev] JinjaThreads

It should work now again (Isabelle/e4716b792713 and AFP/ec3887abf158). Sorry for the trouble, Andreas On 15/09/15 16:41, Makarius wrote: This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9: *** Failed to load theory "Execute_Main" (unresolved "Java2Jinja") *** Failed to load

Re: [isabelle-dev] [isabelle] Code setup for Fraction_Field

Hi Florian, I am continuing this thread on isabelle-dev as you have suggested. 3. For fraction fields over polynomials over rings (rather than fields), one can use subresultants, but I have not been able to find them formalised in Isabelle. Are they hidden somewhere? If not, are there any

Re: [isabelle-dev] NEWS

Hi Florian, I noticed that the new printing interacts strangely with set comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as "Collect (uncurry P)" which I find rather hard to read. Are you aware of this effect and could you please restore the former situation? Best,

Re: [isabelle-dev] HOL-Predicate_Compile_Examples

Hi Makarius, I had a brief look at the unchecked files in Predice_Compile_Examples. I have never worked with these theories, so take my comments with a grain of salt. Predicate_Compile_Quickcheck_Examples: In dc2236b19a3d, Lukas removed the testers which are used in this theory and replaced

[isabelle-dev] goals inserts facts into goal statement

I am trying to replace some of my old usages of case goal_* with the new goals method. In the course, I encountered the problem that goal inserts the facts chained in as additional assumptions of my goals and also for the case bindings. This is unfortunate when I use goals sequenced after rule.

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

On 06/06/15 17:11, Florian Haftmann wrote: So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed

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

, and then destroy the conjunction. I'm currently testing this on testboard (http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010). Cheers, Dmitriy On 09.04.2015 16:11, Andreas Lochbihler wrote: Hi Dmitriy and Jasmin, Thanks for the hint with plugins. That really speeds things up. I also suspect

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

Hi Dmitriy, the code plugin defines a new constant (copy of op =) that is used as equality. datatype x = A | B export_code equal_x_inst.equal_x in SML This is precisely the instantiation of the equals type class. To get it executable (#constructors)^2 equations are proved in a backward

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

Dear BNF and Isabelle/jEdit developers, Today, I noticed that the datatype command in Isabelle/e936c2828bec is sometimes extremely slow. At the end of this mail, there is a large enumeration type where this shows up. Processing this definition on my laptop takes about 4 minutes, but the timing

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

Hi Dmitriy and Jasmin, Thanks for the hint with plugins. That really speeds things up. I also suspect that the timing panel does not include the forked proof tactics. Cheers, Andreas On 09/04/15 15:55, Dmitriy Traytel wrote: Hi Andreas, rather than going dirty, try: datatype (plugins

Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)

It should now work again in 034a4d15b52e. Sorry for the trouble. Andreas PS: The error message is not so obscure if you look at the types. The left hand side talks about hyper-naturals, the right hand side about nat. On 12/03/15 13:56, Andreas Lochbihler wrote: Hi Makarius, You are right

Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)

:Andreas Lochbihler date:Tue Mar 10 16:35:14 2015 +0100 files: src/HOL/NSA/StarDef.thy description: more type class instances The error message of the NSA transfer proof method is a bit obscure. Makarius ___ isabelle-dev

Re: [isabelle-dev] Constructors and the predicate compiler

Dear Florian, I myself have never looked in detail through the implementation of the predicate compiler, but I have been a major user. I previously noticed that it does not go well together with code_datatype. Here are my 50 cents. On the one hand, the predicate compiler generates code

Re: [isabelle-dev] AFP: Sourceforge down

Makarius, I have the impression that your push has not made it to the official afp-code. At least, I cannot see it on http://sourceforge.net/p/afp/code/ci/6ff9a8c6405d04f28365434a0e7bd65ea89aad86/log/ although my commits do show up there. Andreas On 10/02/15 23:08, Makarius wrote: On Tue,

Re: [isabelle-dev] Code preprocessor tracing

Hi Florian, Thanks for all this. 2. Meanwhile, I really like the new simplifier tracing facility and hardly ever use the old [[simp_trace]]. Since the new trace offers a lot of control over the tracing, would it make sense to base the tracing facility on the new one? It would definitely make

Re: [isabelle-dev] Proposal for localized interpretations

Dear developers, Jasmin mentioned to me that his new implementation allows to select which plugins should be applied. Currently, the code generator has its own manager of plugins (Code.datatype_interpretation) and I would be very happy if certain plugins could be disabled selectively upon

Re: [isabelle-dev] Code preprocessor tracing

Hi Florian, Sorry for the long delay until you get an answer, but I wanted to wait until I can port my application from Isabelle2013-2 to 2014. The tracing facility seems to provide some basic means to limit the scope of the tracing. I found the two suggestions for improvement: 1. The

[isabelle-dev] Testing of generated code

Hi all, we have hardly any check that the code generated by the code generator is correct. There is only the checking option of the command export_code. It calls a target language compiler to see whether the compiler accepts the code. Since there are more and more adaptations to serialisation

Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of Library/Quickcheck_Types. Andreas On 18/08/14 18:44, Peter Lammich wrote: However, the constructions might still be useful, as the following comment from Peter Lammich's AFP entry Refine_Monadic shows. (* TODO:

Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

it? Andreas On 11/07/14 15:54, Andreas Lochbihler wrote: Quickcheck does not use these types, because it is currently configures to only use the types finite_1 to finite_3 from Enum, because the finite_types parameter is set by default. Quickcheck internally also seems to work differently depending

Re: [isabelle-dev] ISABELLE_GHC/quickcheck

The Native_Word entry in the AFP contains a number of quickcheck[narrowing] calls that are set up such that they are tested only if ISABELLE_GHC is set. Therefore, there cannot be an error message about quickcheck narrowing if ISABELLE_GHC is not set. Andreas On 19/07/14 21:30, Gerwin Klein

Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

: On 11/07/2014 13:43, Andreas Lochbihler wrote: Quickcheck_Types defines a number of artificial types that quickcheck can use to instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them with int provided that the sort constraints do not prevent

Re: [isabelle-dev] Old 'defs'

There's one use in JinjaThreads which does not fit into the overloading scope: The constants sc_spurious_wakeups are declared in MM/SC_Collections.thy and MM/SC.thy, but intentionally not defined. This expresses that the remaining proofs are independent of the value of the constant, which is in

Re: [isabelle-dev] unit :: complete_boolean_algebra – 697e0fad9337

Hi Florian, the simproc unit_eq in http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78 rewrites anything of type unit to (), so there's no need to declare the definitions introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def,

Re: [isabelle-dev] Remaining uses of Proof General?

Thanks a lot. Andreas On 12/05/14 20:07, Florian Haftmann wrote: 1. Violation of well-sortedness constraints: type ... not an instance of ... declare [[show_sorts]] code_thms constant to be exported Then, I use educated guessing and Emacs' incremental search to navigate the code equations

Re: [isabelle-dev] Remaining uses of Proof General?

On 02/05/14 16:16, Makarius wrote: On Tue, 29 Apr 2014, Andreas Lochbihler wrote: text ‹ @{term ‹A \un B›} › Here the \un works as expected -- the cartouche remains intact independently of its content, as long as the funny parentheses are nested properly. But this correct nesting

Re: [isabelle-dev] Remaining uses of Proof General?

Hi Makarius, On 28/04/14 23:10, Makarius wrote: a) Given some text like definition foo where foo = ... when I add an attribute like [simp]: after the where, I get a symbol completion popup to replace the : with the element sign. Usually, my next thing is to move the cursor with the cursor

Re: [isabelle-dev] Remaining uses of Proof General?

On 28/04/14 23:18, Makarius wrote: On Mon, 28 Apr 2014, Andreas Lochbihler wrote: 2. Reactivity when processing large files With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger project like JinjaThreads, every now and then, Isabelle changes the background

Re: [isabelle-dev] Remaining uses of Proof General?

On 28/04/14 22:25, Makarius wrote: On Mon, 28 Apr 2014, Andreas Lochbihler wrote: My main usage of PG is when I want to construct a complicated proof method call like (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp del: ...)+ that collapses an apply script

Re: [isabelle-dev] Remaining uses of Proof General?

Hi Makarius, Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to working on small projects or refactoring existing sources. I really like the negative line spacing

Re: [isabelle-dev] Issues with interpretations

Hi Jasmin, 1. As long as we define new interpretations (hook types) in the HOL image, we can reorganize the imports to avoid the evil scenarios. Problems arise when users define their own interpretations. I already ran into scenario 3 without registering my own interpretations just by

Re: [isabelle-dev] 'specification' and 'ax_specification'

I myself found specification quite convenient and use it occasionally, e.g., in AFP/Containers/Set_Linorder and a number of my private developments. It's a useful shortcut to a definition with SOME and deriving the properties later with someI. It would be good if it works with contexts. I have

Re: [isabelle-dev] smt2

Hi Jasmin, On 14/03/14 14:18, Jasmin Blanchette wrote: Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting up Quickcheck (and GHC) so that it uses the narrowing strategy. I

Re: [isabelle-dev] smt2

Hi Jasmin, On 14/03/14 16:05, Jasmin Blanchette wrote: Hi Andreas, Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler andreas.lochbih...@inf.ethz.ch: On 14/03/14 14:18, Jasmin Blanchette wrote: Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to depend

[isabelle-dev] Pushing to AFP fails

I am trying to push a changeset to Coinductive to the AFP, but I always get the following error message: remote: abort: could not lock repository /hg/p/afp/code: Permission denied abort: unexpected response: empty string Until last week, hg push used to work well. Has anything changed?

Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function

Hi Jasmin, On 12/02/14 12:11, Jasmin Blanchette wrote: Hi Andreas, I saw that you used the discriminator =, but we already have functions Option.is_none and List.null. So far, they have been mainly used for code generation, but I have found them very convenient in in my codatatype usages

Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function

Hi Jasmin, On 13/02/14 13:47, Jasmin Blanchette wrote: Hi Andreas, Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler andreas.lochbih...@inf.ethz.ch: In summary, I do not want to replace _ = None and _ = [] with null and is_none, I'd just like to make null and is_none somewhat official. I

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

Hi Florian, a) Char_ord and List_lexord are not tied together, i.e., a user could import List_lexord, but not Char_ord, define his own version of order on String.literal and the generated Haskell code compiles, but it is unsound (even without any further adaptations by the user). One could

Re: [isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]

Hi Florian, Just a remark on http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on lexicographic orderings in List.thy is now numerous enough but still self-contained to justify a separate theory Lexorder.thy. I agree that a separate theory would be nice. But before doing

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

not compile. Do you have any ideas or opinions on that? Best, Andreas PS: Similar problems already occur for the size instance of String.linorder in Isabelle2013-1, so linorder is not the only problematic case. On 19/11/13 17:32, René Neumann wrote: Am 19.11.2013 17:10, schrieb Andreas

Re: [isabelle-dev] [isabelle] General code_abort'd constant

Hi Florian, in 2b761d9a74f5, I now have replaced Predicate.not_unique with Code.abort. I decided to leave Enum.the as is, because there is a special translation for the Eval target such that Enum.the raises Match instead of Fail (although I do not know whether the specific setup is

Re: [isabelle-dev] [isabelle] New representation of naturals in Code_Target_Numeral decreases generated code performance

Hi Florian, newtype in Haskell is not always for free, see for example Joachim's blog post: http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html Andreas On 19/09/13 12:58, Florian Haftmann wrote: Hi Peter, When using Code_Target_Numeral instead of the old

Re: [isabelle-dev] [isabelle] General code_abort'd constant

Hi Jasmin, I moved this thread from users to devel, because we are now referring to changesets ;-). I would appreciate if all these code_aborts that you mention were consolidated to use Code.abort. I second this. Cf. http://goo.gl/4kR3vu :) See now 788730ab7da4, which replaces all

Re: [isabelle-dev] including raises Attempt to perform non-trivial merge of theories

2013, Andreas Lochbihler wrote: I get the error Attempt to perform non-trivial merge of theories when I include a bundle from another theory and there are at least two imports. In the attachment, there's an example. This should work in Isabelle/ef65d5ee60cf. Are there any remaining problems

[isabelle-dev] conflict between code_identifier constant and module_name

Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I am having trouble using the greater capabilities of code_identifier. I would like to assign a constant to a different module, say code_identifier constant replicate \rightharpoonup (SML) My_Module.rep

[isabelle-dev] including raises Attempt to perform non-trivial merge of theories

Dear all, in Isabelle abd760a19e22, I get the error Attempt to perform non-trivial merge of theories when I include a bundle from another theory and there are at least two imports. In the attachment, there's an example. Best, Andreas Scratch.thy Description: application/extension-thy

Re: [isabelle-dev] Problems with Code-Generator

Hi René, Florian has reworked the setup for target language numerals. I can at least explain why you run into the error and provide a workaround. Code_Target_Nat implements the type nat as an abstract type (code abstype) with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must

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

Hi Christian, the two different size functions become relevant as soon as you have a polymorphic datatype such as datatype 'a foo = Foo 'a | Bar 'a foo Then, foo_size takes size function for every type variable as additional parameters and takes them into account, whereas size ignores

Re: [isabelle-dev] Should code_abort remove the corresponding code equations?

Hi Florian, On 18/07/13 12:00, Florian Haftmann wrote: Should code_abort remove the code equation for test? Otherwise the resulting program might be non-terminating. I have often run into this problem myself, too, especially in case of non-termination. I would find it sensible that code_abort

Re: [isabelle-dev] Should code_abort remove the corresponding code equations?

Hi Johannes, I have often run into this problem myself, too, especially in case of non-termination. I would find it sensible that code_abort deletes the code equation. Andreas On 09/07/13 15:28, Johannes Hölzl wrote: Hi *, code_abort does not remove the corresponding code equations (in

Re: [isabelle-dev] AFP sitegen

Sorry for the confusion, I never ran sitegen.py myself because I thought that to be the priviledge of the editors. As Gerwin has found out, I dropped these links manually in 376347e6131a because they all were broken after the update on sourceforge. I decided not to update them for three

Re: [isabelle-dev] I don't understand isatest AFP report

Here's a summary of the story with Containers: AFP/db25a6127308 to AFP/58dc11da7731 add the Containers entry to AFP-devel in the version that works with Isabelle2013. In AFP/664abd899c58, Gerwin dropped the import of Code_Char_ord that Florian removed in Isabelle/599ff65b85e2. This

[isabelle-dev] Problem with simproc enat_eq_cancel

Dear all, in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be something wrong with the enat_eq_cancel simproc in Extended_Nat. Can someone please look into this? Here's a minimal example: theory Scratch imports ~~/src/HOL/Library/Extended_Nat begin definition epred ::

Re: [isabelle-dev] Order of sublocale declarations

Hi Amine, the error message in the second case is only delayed: You get it, once you open the AB context again (context AB begin). In the first case, it shows up immediately, because the sublocale command already constructs the context AB enriched with B. Best, Andreas On 01/31/2013 12:48

Re: [isabelle-dev] Order of sublocale declarations

? Amine. On 01/31/2013 02:04 PM, Andreas Lochbihler wrote: Hi Amine, the error message in the second case is only delayed: You get it, once you open the AB context again (context AB begin). In the first case, it shows up immediately, because the sublocale command already constructs the context AB

Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations

Hi Makarius, Side remark: Does anybody remember a use of the 'apply_end' command? Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they could be fused into the qed. However, I regularly use apply_end when I develop the method call for qed to finish off all the

Re: [isabelle-dev] JinjaThreads does not compile

Hi Stefan, while doing a testall on the AFP, I noticed that JinjaThreads no longer compiles. I get the error *** exception Match raised (line 146) *** *** At command ML (line 145 of /mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy) This should be now fixed in

Re: [isabelle-dev] Nominal and FinFuns from the AFP

. This possibly also applies to the where clause although I did not need that for FinFun. Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721

Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)

explicitly instantiate key in the induction method via the taking clause. Otherwise, key is left as an unbound variable in the goal state. For example: proof(induct xs taking: concrete_key rule: sequences_induct) Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler

Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)

. key x \le key y) xs) ys \Longrightarrow P xs (y#ys) shows P xs ys using assms(2-) assms(1) apply(induction_schema) Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49

Re: [isabelle-dev] Open Issues with JinjaThreads entry

plus a few more when the heap image is written. Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu

Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML

and Andreas, there is another occurrence of gconv_rule in Provers/blast.ML (in function timing_depth_tac). Since the exception is thrown when invoking blast, this occurrence of gconv_rule may be the culprit. -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher

Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML

an exception handler. But I could be wrong, as such checks may be done elsewhere. Does anybody else have a suggestion? Larry Begin forwarded message: From: Andreas Lochbihler andreas.lochbih...@kit.edu Date: 27 May 2011 14:51:27 GMT+01:00 To: isabelle-users isabelle-us...@cl.cam.ac.uk Subject

Re: [isabelle-dev] Proof General 4.1pre

Are there still users of PG 3.x with recent Isabelle snapshots or versions from the repository? I am using PG 3.7.1.1 with XEmacs 21.4.21 and a recent version from the Isabelle repository. My motivation for not switching is that PG 4.x did not seem to work with XEmacs when I tried, and I have

[isabelle-dev] Error message Failed to prepare dependency graph

Hi all, I tried to build (my own version of) JinjaThreads with the Isabelle repository version 8cce3a34c122, but it failed with the error message Failed to prepare dependency graph. The log of the run ends with: Loading theory JinjaThreads ### Rule already declared as safe introduction

  1   2   >