Re: [isabelle-dev] Analysis not building

2019-02-03 Thread Bertram Felgenhauer
Florian Haftmann wrote: > > HOL-Analysis can’t be built (reproducibly) with the latest version > > (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis with Isabelle-24bbc4e30e5b and manual

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-28 Thread Bertram Felgenhauer
Makarius wrote: > There was indeed something odd with sharing: David Matthews has changed > that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46). I may give it another try later... > > Hardware: > > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD > > > > Common build

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-25 Thread Bertram Felgenhauer
Bertram Felgenhauer wrote: > Makarius wrote: > > So this is the right time for further testing of applications: > > Isabelle2018 should work as well, but I have not done any testing beyond > > "isabelle build -g main" -- Isabelle development only moves forward i

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-23 Thread Bertram Felgenhauer
Makarius wrote: > On 22/01/2019 12:31, Bertram Felgenhauer wrote: > > Makarius wrote: > >> So this is the right time for further testing of applications: > >> Isabelle2018 should work as well, but I have not done any testing beyond > >> "isabelle build -g

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Bertram Felgenhauer
Makarius wrote: > So this is the right time for further testing of applications: > Isabelle2018 should work as well, but I have not done any testing beyond > "isabelle build -g main" -- Isabelle development only moves forward in > one direction on a single branch. I have tried this with

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

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote: > On 08/11/2018 14:59, Bertram Felgenhauer wrote: > >> > >> I've misunderstood the problem. You intend to invoke old-style > >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > >> Isabelle/ML sessions the

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

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: > > Makarius wrote: > >> Nonetheless, it is still possible to use "isabelle ghc" without stack: > >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the > >> Isabel

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

2018-11-08 Thread Bertram Felgenhauer
Makarius wrote: > Nonetheless, it is still possible to use "isabelle ghc" without stack: > you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the > Isabelle settings mechanism to override ISABELLE_GHC with the > stack-based tools. After purging $ISABELLE_STACK_ROOT, `isabelle ghc`

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

2018-11-07 Thread Bertram Felgenhauer
Makarius wrote: > *** System *** > > * 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

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

2016-08-08 Thread Bertram Felgenhauer
the second for cancellation and `multp`, `multeq`. See the attached file. Cheers, Bertram # HG changeset patch # User Bertram Felgenhauer <bertram.felgenha...@uibk.ac.at> # Date 1470657709 -7200 # Mon Aug 08 14:01:49 2016 +0200 # Node ID 852c841c2ecde57bd9d0695edbad5b392ab418b5 # Parent

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

2015-11-07 Thread Bertram Felgenhauer
Hi Florian, > > This email refers to the following commit: > > > > http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 > > > > code abbreviation for mapping over a fixed range > > > > Is there a specific reason for this code equation: > > > > "map_range f (Suc n) = map_range f n @

Re: [isabelle-dev] AFP devel not reachable

2015-07-20 Thread Bertram Felgenhauer
David Cock wrote: Apparently they had a storage system issue, and obviously didn't have a tested recovery plan. There's some more information here: http://sourceforge.net/blog/sourceforge-infrastructure-and-service-restoration/ In short, they are working on it, and interestingly, they are

[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

2012-05-07 Thread Bertram Felgenhauer
Dear Isabelle developers, the Haskell code generator of Isabelle currently emits contexts for data and newtype generates, e.g. (from CeTA): newtype (Linorder a) = Rbt a b = Rbt (Rbta a b); The sole effect of such contexts is that the programmer must provide a (Linorder a) context wherever Rbt

Re: [isabelle-dev] Isabelle_11-Sep-2011

2011-09-30 Thread Bertram Felgenhauer
Dear Makarius and René, However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a problem for Mac OS Lion users: Many special characters like == \in, = are not displayed correctly which makes working inconvenient. Under