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
> >
> >http://cl-informatik.uibk.ac.at/~thiem
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
Lars Hupel wrote:
> I was trying to update to the repository version today, but:
>
> $ bin/isabelle components -a
> ### Missing Isabelle component: "/home/lars/.isabelle/contrib/jdk-7u40"
> Getting "http://isabelle.in.tum.de/components/jdk-7u40.tar.gz";
> Unpacking "/home/lars/.isabelle/contrib/jd
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 ho
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 @ [
Tobias Nipkow wrote:
>
> I am all in favour of a variation of "add" - it corresponds nicely to "+".
> Of course not "add" by itself, that is too generic. How about
>
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"
I like "add#".
Will the introdu
the second for cancellation
and `multp`, `multeq`. See the attached file.
Cheers,
Bertram
# HG changeset patch
# User Bertram Felgenhauer
# Date 1470657709 -7200
# Mon Aug 08 14:01:49 2016 +0200
# Node ID 852c841c2ecde57bd9d0695edbad5b392ab418b5
# Parent 1e7c5bbea36dd2dd56705630f8e456de9
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 ISA
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` co
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
> >> Isabelle se
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
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 Isabelle20
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
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
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 flag
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 init-component
16 matches
Mail list logo
