Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

>> Are there any issues remaining on this thread after >> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? > > I get this failure on my regular Ubuntu 18.04: > > *** Failed to load theory "HOL-Library.Library" (unresolved > "HOL-Library.Finite_Map") > *** Code check failed for OCaml:

Re: [isabelle-dev] [Isabelle-ci] Build failure in Isabelle+AFP (slow)

I'm note sure what's going on here. It appears to be a spontaneous dropout of the OCaml environment, sporadically: in session Native_Word, theory ~~/afp/thys/Native_Word/Bits_Integer.thy seems to success, whereas in e.g. Iptables_Semantics it fails. I did not experience anything like that on

Re: [isabelle-dev] NEWS

Am 13.03.19 um 20:57 schrieb Lars Hupel: >>   isabelle ocaml_opam install zarith > > This should ideally happen on-the-fly from within Isabelle/ML. Or maybe as implicit part of isabelle ocaml_setup ? Florian signature.asc Description: OpenPGP digital signature

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

Are there any issues remaining on this thread after http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? Cheers, Florian Am 24.06.18 um 22:29 schrieb Makarius: > On 07/06/18 15:22, Lars Hupel wrote: >>> Does this minimal approach make any sense, and solve the imminent >>>

[isabelle-dev] Current AFP problems

isabelle: 03bc14eab432 tip afp: 16e89cda027a tip > Smooth_Manifolds FAILED > (see also > /home/haftmann/data/tum/isabelle/master/heaps/polyml-5.8_x86_64_32-linux/log/Smooth_Manifolds) > ### \finite ?S; \T\?S. closed T\ > ### \ closed (\ ?S) > ### Rule already declared as introduction (intro) >

[isabelle-dev] Specification packages in Isabelle/HOL, particularly primrec

Hi all, after 3bfa28b3a5b2 (followed-up by AFP d058960a13d6) the matter of affairs with specification packages is as as follows: The prototypical specification interface is of shape val add_specification: spec -> local_theory -> result * local_theory where »spec« is the input specification

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

Am 14.02.19 um 13:34 schrieb Makarius: > On 14/02/2019 12:04, Florian Haftmann wrote: >>>> At the moment I am thinking whether the old approach of checking >>>> everything except the computations can be restored without using fancy >>>> low-level stuff. Ma

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

>> At the moment I am thinking whether the old approach of checking >> everything except the computations can be restored without using fancy >> low-level stuff. Maybe by a locale. > > This is indeed a bit fragile. I used to make manual tests of > Flyspeck-Tame over some time, but now ignore

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

Am 10.02.19 um 17:01 schrieb Makarius: > On 04/02/2019 14:17, Makarius wrote: >> On 04/02/2019 10:37, Lars Hupel wrote: >>> Is this related to the latest Poly/ML changes? The "slow" job still runs >>> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware >>> is 8-core LRZ VM. >>

Re: [isabelle-dev] Analysis not building

> HOL-Analysis can’t be built (reproducibly) with the latest version > (76f2d492627e). It simply dies, no error message. I cannot reproduce this. ML_PLATFORM="x86_64_32-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--maxheap 9G" Have you tried a fresh build or delete the corresponding log

Re: [isabelle-dev] NEWS: generated code as proper theory export

>> Maybe the »checking« should just be a variant of the regular export. >> >> Hence the modification could be quite conservative: >> >> export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME ) >> ( file … | ( prefix … ) ( checked ) ) >> >> where »file« denotes a relative root

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

Hi Lars, Am 22.01.19 um 22:34 schrieb Lars Hupel: > It is admittedly a complicated incantation, but here you go: > > $ cat test.ml > let x = Z.one;; > let _ = print_endline (Z.to_string x);; > > $ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith > -linkpkg test.ml > > $

[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

Hi all, as of 82f57315cade (followed-up by AFP bf62184), the still occasionally seen Local_Theory.reset invocations are gone, conveniently replaced by Local_Theory.subtarget_result. I'm considering pushing that even further: specification tools should by contract provide a »clean« definitional

Re: [isabelle-dev] NEWS: generated code as proper theory export

Hi Makarius, > * Are there remaining uses of 'file' with empty name? Is the virtual > file-system browser sufficiently convenient to inspect results > interactively? I checked the file system browser and would be quite content with it; as a bonus you can then make use of the syntax

[isabelle-dev] NEWS: generated code as proper theory export

Code generation: command 'export_code' without file keyword exports code as regular theory export, which can be materialized using tool 'isabelle export'; to get generated code dumped into output, use 'file ""'. Minor INCOMPATIBILITY. This refers to e02bdf853a4c and opens opportunities to get

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

>> Anyway, I am uncertain about the name »poll«. > > From https://en.wikipedia.org/wiki/Cardinality > > "Two sets A and B have the same cardinality if there exists a bijection from > A to B, that is, a function from A to B that is both injective and > surjective. Such sets are said to be

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

> I am inclined to introduce these definitions: > > definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) > where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" > > definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50) > where "eqpoll A B ≡ ∃f. bij_betw f A B” > > They allow,

Re: [isabelle-dev] NEWS: support for GHC

> * Support for Glasgow Haskell Compiler via command-line tools "isabelle > ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack". > Existing settings variable ISABELLE_GHC is maintained dynamically > according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER. Just a side

Re: [isabelle-dev] AFP/HLDE

> Can 'export_code' do that, with a slight modification to produce formal > exports via Export.export? That what indeed be feasible. Instead of "file", a keyword like "prefix" could be given to "export_code". I will put this into my pipeline to implement, but it will take some time until this

Re: [isabelle-dev] AFP/HLDE

Dear all, > It seems to deliver an executable tool for later use elsewhere, but the > implementation is very fragile. > > We could take it as a model to get such a task right. the situation wrt. generated code is indeed somehow baroque. I am aware of the following layers / approaches: a)

Re: [isabelle-dev] Frag / Poly_Mapping

Just my five cent: instead of thinking about *integrating* the developments, I'd suggest to distill their *common essence* into a generic base theory, which would indeed be dedicated to functions with finite support. First-letter abbreviations are not very self-explanatory though. So I'd go with

Re: [isabelle-dev] Explorer.thy [was: performance problems]

Hi all, Am 12.09.2018 um 11:12 schrieb Lawrence Paulson: > I regard it as indispensable. But it does need better pretty printing. > Also I greatly prefer the if/for format to assume/fix. Am 12.09.2018 um 12:12 schrieb Mathias Fleury: > I have my own version of explore >

Re: [isabelle-dev] Purpose of guess_infix

Hi Makarius, I guess this had something to do with Haskabelle, taking into account its fundamental design flaw to write terms on its own rather than having Isabelle's existing printing doing the job. Since there is no reference left, it can be safely discarded. Cheers, Florian Am

Re: [isabelle-dev] Explorer.thy [was: performance problems]

>> On 7 Sep 2018, at 19:18, Makarius wrote: >> >> I can't try it out, since theory "Explorer" is missing. > > Attached. A very cool thing. Nice to see that old draft from 5 years ago. I would still agree that such a tool would be tremendously useful, but before going into the distro it would

Re: [isabelle-dev] Problems with newline in String.literal

For the record: this issue has been resolved in http://isabelle.in.tum.de/repos/isabelle/rev/25b431feb2e9. Cheers, Florian Am 05.09.2018 um 10:32 schrieb Thiemann, René: > Dear all, > > I’m currently changing the error messages in our formalization from the > “string” type to >

Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

> Is it right for this theory to base itself on HOL.Deriv rather than > Complex_Main? > > Larry > > section ‹Polynomials as type over a ring structure› > > theory Polynomial > imports > HOL.Deriv > "HOL-Library.More_List" > "HOL-Library.Infinite_Set" > Factorial_Ring > begin I don't

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

>>> So we could provide "isabelle opam" as wrapper for something like "opam >>> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle >>> opam_init" for the specific compiler version setup. Our component wiring >>> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

> No matter whether we decide to stick with Num or migrate to Zarith, the > code generator needs to be updated to not link against "nums.cma" directly: > > val compile_cmd = > "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^ > " -I " ^ File.bash_path path ^ > "

[isabelle-dev] HOL-ODE-Numerics FAILED

isabelle: 4acc029f69e9 tip afp: c0882468fab2 tip > HOL-ODE-Numerics FAILED > (see also > /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics) >thm -> > int -> >int -> > int -> >int -> > (int * int * string) list -> >

Re: [isabelle-dev] Cannot build HOL (again)

Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp? Florian Am 21.05.2018 um 16:23 schrieb Lawrence Paulson: > Well, it worked on the third attempt. Same as two weeks ago. My guess is that > it pauses to wait for some resource: when it stalls, the process is still

Re: [isabelle-dev] HOL-Algebra

Hi all, just a few comments on my behalf. >> We’ve decided that Group-Ring-Module is irremediable, and are using it >> only as a list of useful results that need to be done again. Seems to make sense. > Just one oddity in HOL-Algebra: It claims canonical theory names like> > "Group", "Ring",

Re: [isabelle-dev] Slowdown of ConcurrentGC

Hi Makarius, > I have studied this a bit further. The interval > 75130777ece4:d45b78cb86cf contains more than just the string type > change, but it is still the main thing. Here are also other sessions in > similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498: > > * faster:

Re: [isabelle-dev] Bad session structure: may cause problems with theory imports

Hi Larry, I guess you have to update your local AFP clone also. Hope this helps, Florian Am 25.04.2018 um 18:03 schrieb Lawrence Paulson: > In the past couple of days, upon launching Isabelle jEdit, I get an alert box > with the message above and the attached text. Any ideas? > >

Re: [isabelle-dev] NEWS: Latex errors

> *** Document preparation *** > > * Command-line tool "isabelle document" has been re-implemented in > Isabelle/Scala, with simplified arguments and explicit errors from the > latex process. Minor INCOMPATIBILITY. That explicit error reporting is a great thing missed for so long!

[isabelle-dev] Haskabelle unmaintained

Hi all, I see that the old Haskabelle website is still a regular part of the Isabelle website: http://isabelle.in.tum.de/haskabelle.html Since Haskabelle is no out of maintainance it is outdated and should be removed. What is the recommended procedure for this? Cheers, Florian --

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

> They are just identifiers and I don't think they are computed with. > However, I don't intend to change formalization beyond a global > implementation of int by some fixed size integers, if that can be done > easily. Otherwise we live with the increase in runtime from 7:20 to 8:20. Hence a

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

Dear all, > The idea above is to provide an option for the HOL codegen that is used > specifically for applications like Flyspeck-Tame. It is mainly a > question to codegen experts, if that can be done easily. streamlining execution of Flyspeck-Tame without risking its integrity is a struggle

Re: [isabelle-dev] NEWS: more options for "isabelle jedit"

Dear Makarius, > *** Prover IDE -- Isabelle/Scala/jEdit *** > > * The command-line tool "isabelle jedit" provides more flexible options > for session selection: > - options -P opens the parent session image of -l > - options -A and -B modify the meaning of -l to produce a base > image on

Re: [isabelle-dev] Future of Nat_Transfer

See now http://isabelle.in.tum.de/repos/isabelle/rev/0230af0f3c59. Florian Am 19.10.2017 um 13:56 schrieb Florian Haftmann: > Dear all, > > the nowadays ancient theory Nat_Transfer (essentially providing an > attribute to transfer ad-hoc between theorems on nat vs. in

Re: [isabelle-dev] linordered_semiring_1

See now http://isabelle.in.tum.de/repos/isabelle/rev/a1a4a5e2933a Cheers Florian Am 28.10.2017 um 16:14 schrieb Florian Haftmann: > Hi Akihisa, > > thanks for pointing that out. > > I will take care of this. > > All the best, > Florian > > Am 20.1

Re: [isabelle-dev] linordered_semiring_1

Hi Akihisa, thanks for pointing that out. I will take care of this. All the best, Florian Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa: > Dear Isabelle/HOL developers, > > I propose to make linordered_semiring_1 a subclass of zero_less_one. > > class linordered_semiring_1 = >

Re: [isabelle-dev] Unexpected auto indent in 13a1081961d2

>> the attached theory is the (unexpected) result of typing its content >> naively and relying on auto indent. >> >> Do others experience the same or is it maybe a settings problem? > > Can you check $ISABELLE_HOME_USER/etc/preferences if there are any > changes on jedit_indent_input,

[isabelle-dev] Unexpected auto indent in 13a1081961d2

Dear all, the attached theory is the (unexpected) result of typing its content naively and relying on auto indent. Do others experience the same or is it maybe a settings problem? Cheers, Florian -- PGP available:

Re: [isabelle-dev] Towards the Isabelle2017 release

Hi Rene, > = > locale foo = fixes f :: "nat => nat" > assumes f_mono[termination_simp]: "f x <= x" > begin > > fun bar :: "nat => nat" where > "bar 0 = 0" > | "bar (Suc x) = Suc (bar (f x))" > > end > > definition com where > [code del]: "com = foo.bar id" > > interpretation foo id

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

Hi Clemens, >> 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. sorry, I didn't

Re: [isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

> Is it intentional that the "Computational_Algebra" theory does not > import "Polynomial_Factorial"? Yes. Polynomial_Factorial requires Field_as_Ring, which does a substantial modification to the type class hierarchy, pulling it apart from long-established traditions in HOL-Main. I have been

Re: [isabelle-dev] Towards the Isabelle2017 release

Am 24.08.2017 um 22:39 schrieb Manuel Eberl: > On 2017-08-24 17:34, Florian Haftmann wrote: >> I would still appreciate if someone would take the comment »Deviates >> from the definition given in the library in number theory« as a starting >> point to reconcile that de

Re: [isabelle-dev] Towards the Isabelle2017 release

For the final record: > \phi is the result of a simple typo accident see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc > Concerning \mu and \nu, I am currently investigating whether an import > swap could re-establish the situation known from Isabelle2016-1 see

Re: [isabelle-dev] Towards the Isabelle2017 release

Hi Rene, > - In the NEWS I read about freeing short constant names like the > “Renamed ii to imaginary_unit in order to free up ii as a variable”. > I definitely support this kind of change, but at the same time found > quite the opposite in HOL-Algebra: > If one imports

[isabelle-dev] Problem in AFP

isabelle: 9a4c049f8997 tip afp: af801987e595 tip Running Separation_Logic_Imperative_HOL ... *** Undefined fact: "sum_list_update_nat" (line 598 of "/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy") *** At command "from" (line 598 of

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

Just for the record: * Topological_Spaces.subseq has already been present before 2007 in HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7) * strict_mono has entered in 2009, see abefe1dfadbb Hence we have the typical situation that a generalized constant subsumes a more ancient unconsciously. Cheers,

Re: [isabelle-dev] scala-2.12.2

See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559 Florian Am 23.06.2017 um 08:43 schrieb Lars Hupel: >> The patch is now running on testboard: >> . > > Unfortunately, this patch did not work out. > >

Re: [isabelle-dev] scala-2.12.2

> Alternatively, Florian might offer some insight why he set up the code > equations for that particular constant in that way (see "String.thy", > where a ML snippet generates 256 code equations). Note that large > pattern matches on the JVM should be avoided, lest we violate the 64k > method

[isabelle-dev] Issue in AFP

> isabelle: 20304512a33b tip > afp: 644957b424ee tip > JinjaThreads FAILED > (see also > /srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads) > ***(\T. > ***typeof\<^bsub>h\<^esub> v = > ***

Re: [isabelle-dev] scala-2.12.2

Am 11.06.2017 um 09:01 schrieb Florian Haftmann: >> It definitely looks like scala-2.12.2 causes non-termination, e.g. of >> src/HOL/Codegenerator_Test/Generate.thy -- I have opened that file in >> isabelle jedit and waited for approx. 30min; a batch build of >> HO

Re: [isabelle-dev] scala-2.12.2

> It definitely looks like scala-2.12.2 causes non-termination, e.g. of > src/HOL/Codegenerator_Test/Generate.thy -- I have opened that file in > isabelle jedit and waited for approx. 30min; a batch build of > HOL-Codegenerator_Test ran into timeout of 2h. > > Maybe Florian has an idea. Btw. I

[isabelle-dev] Build Problem in JinjaThreads

isabelle: 3bec939bd808 tip afp: 09eedef13195 tip > *** {n. enat n < llength stls \ > *** (case lnth stls n of > ***(s, tl, s') \ \ \move s tl s')} :: > *** nat set > *** > *** Coercion Inference: > *** > *** Local coercion insertion on the operand failed: > *** Cannot generate

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

>> Are there good ideas how to do it with Binomial? Thus we could get rid >> of the Pre_Main theory from f533820e7248. > > The import could be changed e.g. to Groups_List. > > Desirable would also be to split the theory into Factorial and Binomial, > to raise awareness of existing combinatorial

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

Am 25.04.2017 um 11:06 schrieb Manuel Eberl: > I think you actually solved that problem by now. If I recall correctly, > it was one of the two dictionary-related problems I told you about a > year ago or so, and then Lars and you solved that problem somehow. > > I can try putting in that code

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

> * Theories "GCD" and "Binomial" are already included in "Main" (instead > of "Complex_Main"). > > > This refers to Isabelle/f533820e7248: the change came up while exploring > theory imports systematically. Normally, only "Main" or "Complex_Main" > should be imported from the HOL session, not

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

whether your issues still persist, or maybe check against a recent ongoing development revision. Hope this helps, Florian > > Best, > Frédéric > > > Fri, 14 Apr 2017 10:09:38 +0200, Florian Haftmann : > > >> Dear Frédéric, >> >> I cannot foll

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

Dear Frédéric, I cannot follow reproduce observation; using the attached theory in Isabelle2016-1, I get > structure Foo : sig > type 'a b > type 'a c > val foo : 'a b -> 'a b > end = struct > > datatype 'a a = A; > > datatype 'a b = B of 'a c a > and 'a c = C of 'a b; > > fun foo x =

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

For the record: Lukas and me have resolved that issue in 721feefce9c6. Cheers, Florian Am 14.01.2017 um 09:33 schrieb Florian Haftmann: > Hi Lukas, > > I am currently stuck with a problem in Quickcheck/Narrowing. > > After about 10 years it came to surface that

[isabelle-dev] NEWS: Computations

Computations generated by the code generator can be embedded directly into ML, alongside with @{code} antiquotations, using the following antiquotations: @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a @{computation_conv …

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

Hi Andreas, that should be fine. I am optimistic that we will manage somehow to work that our during February. Cheers, Florian Am 23.01.2017 um 09:39 schrieb Andreas Lochbihler: > Hi Florian, > > On 21/01/17 16:56, Florian Haftmann wrote: >> unfortunately, a selector

[isabelle-dev] A note on composition in src/Pure/library.ML

Hi all, in http://isabelle.in.tum.de/repos/isabelle/rev/18a6b96f8b00 you see the result of a struggle ongoing for years now to get static vs. dynamic scoping of code generator conversions etc. right. Finally I realized that composition is to blame for. See the following example: ML_val ‹ fun

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

Hi Lukas, thanks for the offer. We have still time before the next release to work that out. Just give me a sign when you start to dig into this. All the best, Florian Am 21.01.2017 um 18:33 schrieb Lukas Bulwahn: > Hi Florian, > > I have been quite busy the last few days and hence

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

ew > scheme. > > I have not tried this, but my guess is that if you do it this way for > the three types narrowing_type narrowing_term narrowing_cons of > Quickcheck_Narrowing and adjust the code equations for the constants in > Quickcheck_Narrowing accordingly, then you ge

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

in > Quickcheck_Narrowing accordingly, then you get back the old behaviour. > > Hope this helps, > Andreas > > On 14/01/17 09:33, Florian Haftmann wrote: >> Hi Lukas, >> >> I am currently stuck with a problem in Quickcheck/Narrowing. >> >> After

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

Hi Lukas, I am currently stuck with a problem in Quickcheck/Narrowing. After about 10 years it came to surface that code generation for Haskell may produce irrefutable patterns due to pattern bindings in let clauses. See ; if I understand

Re: [isabelle-dev] [isabelle] char :: full_exhaustive

Hi Lars, thanks for pointing this out, this was a serious slip in my work. See now http://isabelle.in.tum.de/repos/isabelle/rev/f77b946d18aa Cheers, Florian Am 20.12.2016 um 17:50 schrieb Lars Hupel: > Dear Florian, > > you changed the representation of characters a while back, but it

Re: [isabelle-dev] NEWS: isabelle jedit -R

Great! Am 18.12.2016 um 22:01 schrieb Makarius: > *** Prover IDE -- Isabelle/Scala/jEdit *** > > * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT > entry of the specified logic session in the editor, while its parent is > used for formal checking. > > > This refers to

[isabelle-dev] SysErr when using experimental polyml-test-8529546198aa in JinjaThreads

> isabelle: c48becd96398 tip > afp: 45dd81cdecef tip > Building HOL ... > Finished HOL (0:01:56 elapsed time, 0:05:46 cpu time, factor 2.97) > Building HOL-Word ... > Finished HOL-Word (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.74) > Building JinjaThreads ... > JinjaThreads FAILED > (see

[isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

Hi all, when testing polyml-test-7a7b742897e9 I found out that this breaks session Algebraic_Numbers in the AFP: *** At command "value" (line 42 of "/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy") *** exception Div raised (line 302 of

[isabelle-dev] AFP broken

> isabelle: ae7c11573922 tip > afp: 1bffa6708aea tip > *** [line 5 of > "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] > error: command "theory" expected, > *** but identifier was found: > *** header > *** > *** > *** ^ > *** The error(s) above occurred for theory

[isabelle-dev] Distro broken

> isabelle: fb5c74a58796 tip > afp: c03838321f2a tip > *** No such file: > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Essential_Supremum.thy" > *** The error(s) above occurred for theory "Essential_Supremum" > *** (required by "Probability") (line 15 of >

Re: [isabelle-dev] Old_Number_Theory

Hi Manuel, > I am glad to announce that as of261d42f0bfac, Old_Number_Theory is > finally history. these are good news indeed. One remark on the diff: + src/HOL/Number_Theory/QuadraticReciprocity.thy + src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy This is a formal regression: a proper

Re: [isabelle-dev] Towards the release

> Are there any non-trivial chunks still in the commit/push pipeline that > need special considerations? I have some matter on euclidean division in the pipeline which I hope to be able to finish before my vacation starting at end of October. Florian -- PGP available:

Re: [isabelle-dev] Jenkins maintenance

> Also note that the Mira architects were actually looking at Jenkins at > that time, and pointed out that it was a bit old-fashioned in focusing > on "latest" versions by default and lacking proper changeset identification. The story behind is actually more delicate: mira was started with the

Re: [isabelle-dev] [isabelle] Reconciling FinFuns in Distro and AFP

See now #55256a98f65f. The proofs are really a challenge… Am 16.09.2016 um 22:29 schrieb Lars Hupel: >> This is already ongoing. Johannes and Fabian agreed to replacing the >> finite maps in HOL-Probability with a new representation (cf >> a4acecf4dc21), which will shortly appear in HOL-Library

[isabelle-dev] Theory for discrete log etc.

Hi all, after studying 28d1deca302e I realized that we have now two theories dealing with discrete functions (with one having been hidden in Float.thy for years): Log_Nat.floorlog :: "nat ⇒ nat ⇒ nat" Discrete.log :: "nat ⇒ nat" Log_Nat.bitlen :: "int ⇒ int" Discrete.sqrt :: "nat ⇒ nat"

Re: [isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc

See now 7faa9bf9860b for a related issue. We had a personal conversation that it is very likely that the remaning issues will disappear after the next big envisaged reform of the analysis material. Cheers, Florian Am 07.08.2016 um 10:47 schrieb Florian Haftmann: > Hi Johan

Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

See now rev. 76302202a92d Thanks for contributing! Cheers, Florian Am 08.08.2016 um 14:44 schrieb Bertram Felgenhauer: > Florian Haftmann wrote: >> Hi Bertram, >> >>> How shall we proceed? As I hinted at earlier I do not have (nor want, at >>> this poin

[isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc

Hi Johannes, that change had probably more pervasive effects than intended. E.g. the definition definition (in comm_monoid) operative … and its basic lemmas now produce the following soup of theorems thm inf_top.operative_def sup_bot.operative_def add.operative_def mult.operative_def

Re: [isabelle-dev] Multiset insert

Just an aside: concerning »insert« and »add«, infix syntax would be desirable, e.g. a `insert` X a `add` M similar to Y \union Y N + M which would yield much more readable propositions, esp. wrt. associativity: a `insert` b `insert` X = {a, b} \union X

Re: [isabelle-dev] Multiset insert

>> Tobias wrote: >> >>> How about >>> >>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where >>> "add# x M = {#x#} + M" > > This, however, may produce confusion with multiset union, which is an > instance of the plus type classes, i.e., occupying the name > plus_multiset. To

Re: [isabelle-dev] {0::nat..<n} = {..<n}

erwise implicit in the type. > > Tobias > > On 04/07/2016 21:00, Florian Haftmann wrote: >>> The problem with {..<n} on nat is that you need multiple versions of >>> every lemma involving {m..<n} on nat. Hence I discourage the use of >>> {..<n} on nat

Re: [isabelle-dev] Considered harmful: surj

> Yes I second that. It surely is a good idea to just use it only as a > input translation. See now 6af79184bef3. Florian > > - Johannes > > Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann: >> Hi all, >> >> since cf26dd739

Re: [isabelle-dev] Permutations

once met an algebraist who preferred + for abelian groups and * otherwise, and this makes sense. Cheers, Florian > > - Johannes > > Am Dienstag, den 05.07.2016, 19:40 +0200 schrieb Florian Haftmann: >>> >>> One question: why did you only se

Re: [isabelle-dev] {0::nat..<n} = {..<n}

look at the bright side: >> {0..<n} clearly shows that the set/sum is bounded, something that is >> otherwise implicit in the type. >> >> Tobias >> >> On 04/07/2016 21:00, Florian Haftmann wrote: >>>> The problem with {..<n} on nat is that you need

Re: [isabelle-dev] An experience report on the testboard

Am 04.07.2016 um 23:49 schrieb Lars Hupel: >> The problem I was referring to is that in order to get a deeper idea >> what's going on you want to have a look at the topology of the history. >> However I guess this is closely related to my surprise that not both >> patches to distro and AFP pushed

Re: [isabelle-dev] Permutations

> One question: why did you only set it up for monoid_mult and inverse, > and not as a ab_group_mult? The answer is simple: there is no type class ab_group_mult. Why? Since our multiplicative structures are tailored towards rings where 0 is no part of the multiplicative group. Cheers,

[isabelle-dev] Permutations

Hi all, see 59803048b0e8 for some basic facts about almost everywhere bijections aka permutations. Maybe this will become a convenient coagulation point for various scattered material in the future. It turned out quite ambitious to formulate basic properties, e.g. circularity. I

[isabelle-dev] Bijections

Hi all, in 1a474286f315 I have introduced a locale for (total) bijections, allowing to obtain typical facts like ‹inv f ∘ f = id› by interpretation. The motivation was that most of these facts have not ‹bij› but ‹inj› or ‹surj› as premise, which makes proof complicated due to two lifting

Re: [isabelle-dev] An experience report on the testboard

>> 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and >> await new build run to be scheduled. > > There can currently only be one testboard build running at a time. That > means you should wait to push until the previous run is finished. > > I understand that this is not ideal.

Re: [isabelle-dev] An experience report on the testboard

>> 1. Changesets to dist and AFP exist as hg patches. > > This is currently not implemented. Isabelle testboard will always use > AFP devel and vice versa. It is not possible to test Isabelle testboard > and AFP testboard together. But I regard this as a central use case: if a change to the

Re: [isabelle-dev] {0::nat..<n} = {..<n}

> The problem with {.. every lemma involving {m.. {.. all problems: not all proof methods invoke simp all the time. > > I consider

[isabelle-dev] Considered harmful: surj

Hi all, since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f = UNIV›. This is a little bit unfortunate since an ordinary equation is just hidden in output that way, resulting in lots of casual confusion. I would suggest to turn ‹surj› into a mere input abbreviation, similar to

[isabelle-dev] {0::nat..<n} = {..<n}

Hi all, obviously on natural numbers ‹{0..

[isabelle-dev] An experience report on the testboard

Hi all, I have started to use the testboard and want to excite feedback on my workflow, as well as hint to certain inconveniences in the current setup. 1. Changesets to dist and AFP exist as hg patches. 2. In both repositories: hg push_to_testboard where »push_to_testboard«

  1   2   3   4   5   6   7   >