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

OK. This is running now in testboard: The corresponding changeset is . I have discarded my changeset now, because Florian has pushed an alternative solution. Here it

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

> Where "automatic" means that a single Isabelle administrator (e.g. the > local user) decides to invoke "isabelle ocaml_setup" and do other > Isabelle administration in parallel. Afterwards the ISABELLE_OCAML > settings will be correctly provided by the etc/settings scripts, without > any further

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

> I don't understand what is going on here. I thought I had to set > ISABELLE_OCAML manually for this kind of code export to even do > something. From what I can tell, I did /not/ set ISABELLE_OCAML on my > machine, but I still get that error. Or did that behaviour change somehow? My understanding

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

> 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: "$ISABELLE_ROOT/lib/scripts/ocamlexec" > ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml > *** At command "expor

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

"Unable to increase stack" is one of the various messages that tells you that PolyML has run out of resources. It doesn't really tell you what the problem is though. It might be an actual problem or a temporary problem caused by a machine being overloaded. This is likely connected to the recent

Re: [isabelle-dev] NEWS

Or maybe as implicit part of isabelle ocaml_setup Sure, that could also work. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

isabelle ocaml_opam install zarith This should ideally happen on-the-fly from within Isabelle/ML. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Current AFP problems

> I’m getting no alerts for some reason I don't see any mail delivery issues in the logs. Maybe none of your sessions were affected? Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/

Re: [isabelle-dev] Towards Poly/ML 5.8

After a lot of refinements by David Matthews we are moving towards the new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML version of that number, without being official yet. The Isabelle NEWS already talk about an official release: Is it intentional that the system identi

[isabelle-dev] Timeouts in Flyspeck_Tame

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. https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/1010/consoleFull ___ isabelle-

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

> The standard approach for the latter is to have the other tool directly > import its source format into the theory context within Isabelle/ML, > without the intermediate theory source. Doing this carefully, would even > produce nice PIDE markup for the original sources. PIDE is an IDE for > arbit

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

> What are the remaining uses of these? How much of this can be integrated > into the formal Isabelle session? How much of it is actually obsolete? Hard to tell from a distance, but here's what I gather from reading the Makefiles: – Formal_SSA appears to download some file, unpack it, and compile

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

> In 2012 we eliminated all Makefiles from AFP: I did not know that some > came back, or chose to ignore it. ~/work/afp (default)$ find thys/ -name Makefile thys/Buchi_Complementation/code/Makefile thys/Formal_SSA/Makefile thys/LightweightJava/ott-src/Makefile thys/Sturm_Sequences/guide/Makefile

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

> 1. Gratchk is a similar use-case, where I need to export code, link it > with some external ML code using MLton b/c it's faster, and test the > result for timing regressions. Because gratchk is also bundled with > gratgen, which is implemented in C++, I have not yet put it into the > AFP, b/c tha

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

> But ocamlfind semms not to provide a subcommand to invoke the > interactive OCaml toplevel. What am I missing? The other way round. "ocamlfind" hooks into the toplevel. $ isabelle ocaml_opam config exec ocaml OCaml version 4.05.0 # #use "topfind";; - : unit = () Findlib has been succe

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

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 $ ./a.out 1 You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") wh

Re: [isabelle-dev] mercurial accident

> The problem behind this: Angeliki got administrative push-access to the > Isabelle repository, without anybody at Cambridge showing her how to use it. Before we start blaming individual people, this is not a person problem, but a tooling problem. Industry has figured out this problem years ago.

Re: [isabelle-dev] mercurial accident

> Strip the accidental changes from the repository? Never strip public changesets. > Back out the changes? You can't really back out merges, as far as I know. > Or do a no-op merge from a successor of the last working version? This is also not possible, I think. Do this instead: $ hg revert

Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

* Support for Isabelle command-line tools defined in Isabelle/Scala. Instances of class Isabelle_Scala_Tools may be configured via the shell function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle component). This is nice! Anything on the radar to automate compilation as well, just

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

> The binary provided by Homebrew does not exhibit that problem. I have no > other information beyond that. I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. Interestingly enough, I get Poly/ML warnings of the form: 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_ma

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

> Can you actually explain the problem and its solution? The problem appears to be that the official Stack binaries do not work consistently on El Capitan. The machine I've tried them on is fully updated and has no special software setup. The binary provided by Homebrew does not exhibit that prob

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

> On an El Capitan system, this produces the following error: The problem can alternatively be solved by installing Homebrew's stack version and declaring ISABELLE_STACK="/usr/local/bin/stack" in ~/.isabelle/etc/settings. ___ isabelle-dev mailing list

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. On an El Capi

[isabelle-dev] Slaying the hydra

Yesterday, Tobias observed an interesting problem: $ hg pull pulling from http://isabelle.in.tum.de/repos/testboard/ searching for changes abort: HTTP Error 414: Request-URI Too Long The cause is a combination of that repository being many-headed and Mercurial trying to be too smart about pulling

Re: [isabelle-dev] System migration

> I will update as soon as the migration is completed. Migration completed. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] System migration

Dear Isabelle developers and users, we will perform a large-scala system migration over the next 24–48 hours. The purpose is to move towards the latest Ubuntu 18.04 LTS. Affected will be continuous integration, the AFP, and the AFP submission service. Expect intermittent unavailability and HTTPS

Re: [isabelle-dev] NEWS: support for OCaml / OPAM

> * How to re-init the opam installation, e.g. after changing > ISABELLE_OCAML_VERSION (maybe even in ISABELLE_HOME_USER/etc/settings)? > (Presently I have just removed purged ISABELLE_OPAM_ROOT.) I don't think purging the directory is necessary. It should work out of the box. According to m

Re: [isabelle-dev] AFP/HLDE

> For the ROOT entry there is already 'export_files' in Isabelle2018. This > could be augmented by something like: > > export_action NAME = SCALA > > with a snippet of Scala source that is a function from the resulting > session build to unit. It could invoke build tools for Haskell, Ocaml, > S

[isabelle-dev] NEWS: CakeML compiler

This refers to AFP/c245a746483a and Isabelle/337b8ce5ff8d. The CakeML compiler is now available from within Isabelle/ML. Steps to use: 1) echo 'init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/cakeml"' >> ~/.isabelle/etc/settings 2) echo 'ISABELLE_CC=gcc' >> ~/.isabe

Re: [isabelle-dev] NEWS: discontinued old-style inner comments

> There were a few remaining uses in AFP. Notable changes are > AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources > generated by LEM (!). I don't know how LEM is maintained: it needs to > produce different inner comments next time, and can actually use > \ CARTOUCHE notation unifor

Re: [isabelle-dev] CakeML compiler in the AFP

> Just a side-remark: Fabian Immler has started with some experiments to > use HOL4 with CakeML inside Isabelle. You should keep in contact with > him about progress and possibilities. Of course. I'm aware and we're emailing back and forth. But this is to some extent orthogonal to Fabian's effort

Re: [isabelle-dev] CakeML compiler in the AFP

> What is the meaning for "optional?" for AFP? We don't have any established process for additional components in the AFP. The question is, should this go into "$AFP_BASE/etc/components" or not? > I've briefly tried cake-x64-64 on Linux, Mac OS X 10.10, and Cygwin 64 > from https://isabelle.sketi

[isabelle-dev] CakeML compiler in the AFP

Dear list, I'm considering putting the entire CakeML compiler somewhere so that it is accessible in the AFP. This includes a pretty-printer of (a small subset of) the abstract syntax; together with some ML code that allows one to invoke the compiler, not unlike "export_code ... checking". Note th

[isabelle-dev] datatype_compat: exception Bind

Dear BNF developers, it appears that the "datatype_compat" cannot cope with non-standard bindings. I get an "exception Bind" when trying to invoke "datatype_compat" on a "qualified" or "private" datatype. There's a somewhat satisfactory workaround, which is to use setup ‹Sign.mandatory_path "some

Re: [isabelle-dev] LRZ outage

> I will update as soon as service resumes. All systems operational again. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] LRZ outage

Dear developers, it appears that there is a large-scale LRZ outage. The following services are affected: - AFP submission service - AFP slow tests as well as other machines used privately by various people that are hosted in the Compute Cloud. I will update as soon as service resumes. Che

Re: [isabelle-dev] Testing the QuickCheck setup

Hi Andreas, thanks, you're making some good points. > 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? No, it fails on all of them. > It might be that you have a fairly large

[isabelle-dev] Testing the QuickCheck setup

Dear list, I've been trying to test some QuickCheck generators in the CakeML formalization, like so: Unfortunately, it seems that they fail occasionally. I've tried increasing the timeout, but that still s

Re: [isabelle-dev] Problems connecting to https://isabelle.in.tum.de/repos/isabelle

In the past 2 days the isabelle_cronjob could not connect to https://isabelle.in.tum.de/repos/isabelle -- but it appears to work from most other hosts that I've tried. Maybe some odd change concerning SSL certificates on the server vs. client side? That's indeed strange. There was an issue wit

Re: [isabelle-dev] Towards Isabelle2018-RC1

> I will produce Isabelle2018-RC1 later today, maybe in approx. 3h. > > For that I also need a version of AFP that works. According to , the latest known-good version (except for the "slow" sessions) is Isabelle/1b9462304e1d AFP/2af750da996c ___

Re: [isabelle-dev] Is hgbroy down?

> Apparently so. I'll let our administrators know. Should be up again. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Is hgbroy down?

> ~/isabelle/Repos/src/HOL: hg fetch > remote: ssh: connect to host hgbroy.informatik.tu-muenchen.de port 22: > Operation timed out > abort: no suitable response from remote hg! Apparently so. I'll let our administrators know. ___ isabelle-dev mailing l

Re: [isabelle-dev] Jenkins reconfiguration

Does it mean that the great new hardware is now locked up and exclusively available for Jenkins? That assessment is accurate. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-d

Re: [isabelle-dev] Jenkins reconfiguration

> - The "testboard" job will also be replaced to run Isabelle+AFP > together. Historic builds will be deleted, as they are not relevant for > the official history. I have implemented this now. I'm currently monitoring the situation, but so far, it seems like this sped up the process overall. _

[isabelle-dev] Jenkins reconfiguration

Dear Isabelle developers, you may have already noticed that some Jenkins jobs got reconfigured. The following changes are relevant for developers: - The new job "isabelle-all" runs Isabelle+AFP together, incrementally. This should improve overall performance and avoid double builds. There is, on

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

> I think it works properly now, see Isabelle/f0f83ce0badd + AFP/f7e9efc65d82. Thanks for that. I'll proceed with the systems integration process of that machine now. > I usually measure the CPU time, multiply it by 2, and take the ceiling > towards the next multiple of 300. In principle this mai

[isabelle-dev] LRZ outage

Dear users of the LRZ servers, there appear to be some network and/or capacity problems at LRZ right now, which is also why the "nightly" job failed just now. I hope this will be resolved soon. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.t

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

> But there are still (spurious) issues with some AFP sessions. With high > contention (a total of 64 worker threads at the same time, e.g. with > threads=2 and -j 32), some sessions will run into suspicious timeouts: > > Timing Median_Of_Medians_Selection (2 threads, 25.039s elapsed time, > 44.46

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

>> So far it looks good, but we still need to test all of AFP. > > I will do that today and report my findings. The machine has been busy since yesterday running the distribution and the AFP (except for slow) multiple times using different parameters. The distribution is working fine. But there

Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

David has worked rather quickly and produced the following commit: https://github.com/polyml/polyml/commit/86c52cbd8f6d I have updated the polyml component accordingly in Isabelle/1b8457cc4de8. So far it looks good, but we still need to test all of AFP. I will do that today and report my fin

[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

Dear list, the good news is that we have just received new hardware (Dual Epyc 7601). The bad news is that a current development snapshot (Isabelle/410818a69ee3) exhibits a problem on this hardware. In particular, the session HOL-Corec_Examples doesn't appear to terminate. $ cat .isabelle/

Re: [isabelle-dev] quaternions

> So where does this material belong? Arguably not in Analysis, which is > already too large. Why not a regular AFP entry? Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/i

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

> Does this minimal approach make any sense, and solve the imminent > administrative problems? In particular without a decision yet about > ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC? I tend to agree. Let's fix OCaml to 4.05.0 and we can figure out a good way to upgrade after the

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

> So I would like to focus: > * What (upcoming) maintenance challenges are we facing? There are many applications in the AFP that link generated code to larger developments. For example, Julian Brunner recently updated the CAVA model checker because it is not tested systematically (e.g. nightly),

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 the > res

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

> In practice "their" version means a version in distant past that was the > current one when the author was working on the session. The reason why I suggested it was to avoid one more burden on Isabelle developers: whoever updates the bundled OCaml version, must also adapt whatever arrangements d

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

> I have now experimented a bit with opam-1.2.2 on Linux, Mac OS X, > Windows/Cygwin64. It appears to work quite well, e.g. like this: > > ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0 > > The opam executables only require a few MB. The result in > ~/.isabelle/opam above

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

since approximately Isabelle/e0cd57aeb60c (~1 week): *** Malformed global fact "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict" *** Illegal fixed variable: "s1" *** At command "primrec" (line 164 of "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy") ___

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

> The best way maybe is to introduce a dedicated isabelle tool »ocamlc« > which uses an environment parameter ISABELLE_OCAML as path prefix to > ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc > montage in ML. Yes, but we would still need to figure out how to "peg" a partic

[isabelle-dev] OCaml 4.06.0 drops nums.cma

I've been trying to figure out why some recent updates broke code checking (both in the distribution and the AFP) for OCaml. It turns out that the "nums.cma" module that we rely on for big integer arithmetic got removed from the standard library. This problem will affect anyone on rolling releases

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

> Unknown JAVA_HOME -- Java unavailable After removing .isabelle, you'll have to do the usual incantation to retrieve the components: ./bin/isabelle components -I ./bin/isabelle components -a ___ isabelle-dev mailing list isabelle-...@in.tum.de https://

[isabelle-dev] I/O error in isabelle build

I'm seeing some spurious (?) errors in "isabelle build": 17:15:13 Finished List-Index (0:00:08 elapsed time, 0:00:11 cpu time, factor 1.37) 17:15:13 *** I/O error: /tmp/isabelle-jenkins/process478460358635901180/export2631876 (No such file or directory) I don't understand where these are com

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

> Last known good state is: > > Isabelle/7e349d1e3c95 > AFP/c3cfeceda7a0 We're back to normal now, as of Isabelle/58c9231c2937 AFP/79f64c92d5ae ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/l

Re: [isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

(I meant "non-termination", of course, not "non-determinism".) > Even if it'll terminate eventually (I'll keep it running for a bit > longer), it surely is a sign of a performance degradation. This run (threads=8) confirms that HOL-ODE-Numerics doesn't terminate within 2 elapsed hours: https://c

[isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

Isabelle/763f5a8f3f7f AFP/2b0fc2365a6e I'm unable to build the HOL-ODE-Numerics sessions. Usually, it takes about ~1 hour of CPU time (0:45 on lxcisa*). It's been running for almost 2 CPU hours now on lxcisa0 (threads=10) and over 1:30 CPU hours on my i7 (threads=8). It also doesn't appear to

Re: [isabelle-dev] bad session structure

> I'm getting this message again. What gives? Everything is fully updated. > > ~/isabelle/Repos/src/HOL: hg id > 2e5b737810a6 tip Do you have any uncommitted changes? Maybe in the AFP? ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP' works fine for me. Cheers Lars _

Re: [isabelle-dev] lxisabelle/lxcisa* maintenance

> Jenkins is back online. For technical reasons, lxcisa0 will only become > available again tomorrow. All services operational again. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab

[isabelle-dev] Bad documentation directory

When I clone a fresh copy of Isabelle, or run "hg clean --all", then "isabelle build" fails with the following error message: *** Bad documentation directory: "/home/lars/work/isabelle/src/Tools/jEdit/dist/doc" That directory is not present by default and appears to be only created by "isabelle j

Re: [isabelle-dev] lxisabelle/lxcisa* maintenance

> - Jenkins > - (shell access to) lxcisa0 Jenkins is back online. For technical reasons, lxcisa0 will only become available again tomorrow. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/ma

[isabelle-dev] lxisabelle/lxcisa* maintenance

Dear users of lxisabelle/lxcisa*, on Sunday, I will have to perform necessary maintenance. The following services may be interrupted and/or unavailable: - Jenkins - (shell access to) lxcisa0 In particular, I recommend to not start any new jobs on lxcisa0, as I might have to stop them. Please

Re: [isabelle-dev] NEWS: Latex errors

> * Command-line tool "isabelle document" has been re-implemented in > Isabelle/Scala, with simplified arguments and explicit errors from the > latex process. Minor INCOMPATIBILITY. Featherweight_OCL now fails to build: isabelle document -d /home/lars/.isabelle/browser_info/AFP/Featherweight_OCL/

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

> We are presently testing Poly/ML 5.7.1 by default (see > Isabelle/aefaaef29c58) and there are already interesting performance > figures, e.g. see: > > http://isabelle.in.tum.de/devel/build_status > http://isabelle.in.tum.de/devel/build_status/Linux_A > http://isabelle.in.tum.de/devel/build_statu

Re: [isabelle-dev] AFP statistics

> The devel equivalent is available at > and is re-generated every > time someone pushes to the repository. Currently that one shows wrong > dependency numbers because it hasn't been adapted yet to > session-qualified imports. I'm still working on a prope

Re: [isabelle-dev] AFP statistics

> The AFP statistics https://www.isa-afp.org/statistics.html is very nice > -- I often show the last diagram in presentations, as a proof of success > of Isabelle as application platform over the years. > > Who is actually responsible for this tool? Me and our student Max Haslbeck. It is part of

Re: [isabelle-dev] Towards the Isabelle2017 release

> My plan would be to fork the AFP 2017 release branch tomorrow (around > midnight CET from Mon to Tue). > > There still seems to be quite a bit of ongoing activity - if there is > anything that needs to go into the afp-2017 release, please let me know. One more thing that is of interest to use

Re: [isabelle-dev] isabelle build timing

> The canonical build parameters for this machine appear to be: > > isabelle build -j8 -o threads=6 I find this combination (8*6 = 48 threads) to be surprising, given that that machine has only access to 22 physical (non-HT) cores. Judging from your list below, this is the minimum number of thr

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

Hi Viorel, it's probably easiest to send a patch containing your changes to this mailing list. (Alternatively, a copy of all the files you changed.) Some Isabelle committer can then push this to the testboard which will run the whole AFP. Cheers Lars On 27 August 2017 16:59:44 CEST, Viorel Pre

[isabelle-dev] NEWS: Pattern Aliases

* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax for pattern aliases as known from Haskell, Scala and ML. This is a small library theory providing convenient syntax for defining recursive functions. Tobias is already using this for defining functions over trees. For example

Re: [isabelle-dev] [158c513a39f5] JVM crash

> Lars, maybe you can run the same test on your machine and see what > happens there. I did, and nothing happened for about 100 iterations. I have a Core i7-2600. OS is otherwise identical to Manuel (Arch Linux). > As for Scala, could a problem in the Scala compiler really lead to the > JVM segfa

Re: [isabelle-dev] [158c513a39f5] JVM crash

> on 158c513a39f5, I just had a JVM crash during "isabelle build" when it > was building Isabelle/Scala. (Log attached). I had a similar problem today. Unfortunately I didn't save the logfile. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tu

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

Dear Andreas, > 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

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

Dear users of the code generator, last week I spoke with Florian about some fundamental properties of the code generator. Many Isabelle users are also "power users" of the code generator; in the sense that they exploit many of its facilities (code printing, various attributes, ...). These days th

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

> thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f. Great, thanks! > 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 co

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

Dear BNF experts, a while ago [0] I posted some comments on the "lift_bnf" command. I'm currently in the process of cleaning up the "Finite_Map" theory and found out that now, "lift_bnf" exports the definitional theorems for map/rel/set. In this case, the theorem looks like this: fmmap ≡ λf. Abs

Re: [isabelle-dev] The coming release of Isabelle2017

I currently supervise a student who's investigating proof refactoring. One possible outcome of this would be a tool that also does what you suggested. It's a little too early to tell, though. Cheers Lars On 8 July 2017 23:28:42 CEST, Lawrence Paulson wrote: >No, that’s precisely what I’d like

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

> Incidentally, I wonder if it is possible to locally prefer one of the > two constants, i.e. say that, in the following block, I want "subseq" to > mean "Topological_Spaces.subseq". That might also mitigate the problem > of long qualified names. Here's my unqualified opinion: Makarius already int

Re: [isabelle-dev] scala-2.12.2

> The patch is now running on testboard: > . Unfortunately, this patch did not work out. 22:13:39 *** Failed to finish proof (line 62 of "~~/src/HOL/Library/Code_Target_Nat.thy"): 22:13:39 *** goal (1 subgoal): 22:13:39 *** 1. Transfer.Rel

Re: [isabelle-dev] scala-2.12.2

> I took the opportunity to have a look at it and found out it can be done > differently, see attached patch. The patch is now running on testboard: . > The clue about "integer_of_char" is that it had to work regardless > whether HOL chars a

Re: [isabelle-dev] scala-2.12.2

> The guys there are talking about Dotty. Do you think it will be also > taken into account by the regular scalac maintainers eventually? Those are Martin Odersky's students, so it's natural that they want to avoid this in Dotty. I'm confident that the scalac team at Lightbend will also have a lo

Re: [isabelle-dev] scala-2.12.2

> a "StackOverflowError" (in the patmat phase), before I even got a chance > at running this I have investigated this now. It is a regression from Scala 2.11.x to Scala 2.12.x. The offending function is "integer_of_char", which performs a 256-way pattern matching. Maybe this should be implemented

Re: [isabelle-dev] scala-2.12.2

> The scalac part should be OK. The problem is the scala part, i.e. actual > runtime -- presumably the run_cmd here: > http://isabelle.in.tum.de/repos/isabelle/annotate/20304512a33b/src/HOL/Library/code_test.ML#l562 > > I've just made a quick test of HOL-Codegenerator_Test on lxbroy10: it > leads

[isabelle-dev] include option for "sessions" in ROOT

I'm playing around with the new "sessions" feature for qualified imports. I think a prominent use case is to depend on various AFP entries. When I'm working on my local development, I'd like to do this: session Preliminiaries = ... sessions HOL-Library theories HOL-Library.FSet ... sess

Re: [isabelle-dev] scala-2.12.2

> I've just pushed the inverse patch of 94b0da1b242e to testboard, so > we'll see. > > HOL-Codegenerator_Test runs fine (0:14:41 elapsed time). Cheers Lars ___ isabelle-dev mailing list isabelle-

Re: [isabelle-dev] scala-2.12.2

> Maybe we should give it another try? I've just pushed the inverse patch of 94b0da1b242e to testboard, so we'll see. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mail

Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples

> The idea is to have a somewhat manageable chop from > Iptables_Semantics_Examples within the range of a build with standard > parameters (which means x86), merely guarded by "slow" group tag. > > Thus it is visible in tests like "isabelle build -d '$AFP' -a -X > very_slow" that I am doing manual

Re: [isabelle-dev] Splitting of Iptables_Semantics_Examples

> That is the result of spending 1-2 days trying to figure out where the > really big parts of that session are, and what are the problems with > polyml-5.7 -- if these don't get resolved we are in a very bad > situation, sitting on a dead branch with the rather old Poly/ML 5.6. That makes sense.

[isabelle-dev] Splitting of Iptables_Semantics_Examples

Since AFP/b56d94d, the big session Iptables_Semantics_Examples is split into four smaller sessions. This poses a problem for the nightly job, which is running with -j1 and threads=8. The parallelism in the four smaller sessions is much less than the parallelism (factor 3) in the previous big sessi

Re: [isabelle-dev] scala-2.12.2

> After your change d76937b773d9, I still see a non-terminating > HOL-Codegenerator_Test. So in 94b0da1b242e I have switched back to > scala-2.11.8. Interesting. In Jenkins, this commit builds fine: . (I had tested it w

Re: [isabelle-dev] scala-2.12.2

> With Isabelle/a43a079156a6 we are on scala-2.12.2, leaving the 2.11.x > behind. See also Isabelle/d76937b773d9, which repairs a broken code adaptation. Note that `error` had been deprecated for at least one major release cycle. Maybe we should start performing code checks with stricter compile

Re: [isabelle-dev] unable to start Isabelle/jEdit due to error in unused session

Dear Chris, > 2) or there was some easy way (e.g., a flag) to exclude specific > Isabelle components / sessions / ROOT files from checks (without having > to edit "etc/settings"). I believe I have a solution for this problem. For a while now, I've been using a custom Isabelle "launcher" based on

  1   2   3   >