Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

> On 09.11.2018, at 22:34, Makarius wrote: > > On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: >> We probably still have a few occurrences of these, but no problem >> phasing them out. > > In principle it is just a matter of applying "isabelle update_cartouches > -t", but it might

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

We probably still have a few occurrences of these, but no problem phasing them out. Cheers, Gerwin On 09.11.2018, at 10:03, Peter Lammich mailto:lamm...@in.tum.de>> wrote: I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ...

Re: [isabelle-dev] function (default) is legacy feature (since 2010)

> On 24 Sep 2018, at 6:23 am, Makarius wrote: > > Are there any remaining uses of "function (default)"? > > changeset: 41417:211dbd42f95d > parent: 41414:00b2b6716ed8 > user:krauss > date:Wed Dec 29 21:52:41 2010 +0100 > function (default) is legacy feature > > > I

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

> On 20.09.2018, at 22:19, Lars Hupel wrote: > >> 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 don’t think this should go into the AFP,

Re: [isabelle-dev] a question about regulations

Isabelle is distributed under a BSD 3-clause license. The only restrictions for Isabelle itself are (see COPYRIGHT file): * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must

Re: [isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

Good points. I’ve added the slow/very_slow and x64 hints to the documentation now. Cheers, Gerwin > On 15.01.2018, at 07:38, Makarius wrote: > > On 14/01/18 12:42, Clemens Ballarin wrote: >> Dear Maintainers of Isabelle / the AFP, >> >> Where would I find instructions on

Re: [isabelle-dev] [ExternalEmail] Status of afp-devel

https://bitbucket.org/isa-afp/afp-2017 now exists and further commits to afp-devel will not automatically appear there any more. Cheers, Gerwin On 29.09.2017, at 09:16, gerwin.kl...@data61.csiro.au wrote: Imminent. I was waiting for the statistics part to

Re: [isabelle-dev] Status of afp-devel

Imminent. I was waiting for the statistics part to be updated to the new qualified imports, but I think we’ll just handle that one separately. Cheers, Gerwin > On 28.09.2017, at 23:52, Makarius wrote: > > What is the status of the afp-devel repository? > >

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. Cheers, Gerwin > On 9 Sep 2017, at 04:30,

Re: [isabelle-dev] [isabelle] [ExternalEmail] afp-2016-1 branch

Hi Randy, there are a few sessions with the tag “slow” in the AFP, of which Flyspeck_Tame is one. These are tested once a day. All other sessions are tested with each push. Cheers, Gerwin > On 6 Dec 2016, at 12:28 AM, Randy Pollack wrote: > > Gerwin, > > I was

Re: [isabelle-dev] [ExternalEmail] afp-2016-1 branch

As of 61df7b06f131 there is now a new branch afp-2016-1, which will become the new afp release branch when Isabelle2016-1 is released. Any further changes to afp-devel will now by default not show up in this branch. Cheers, Gerwin > On 28 Nov 2016, at 6:08 PM, gerwin.kl...@data61.csiro.au

[isabelle-dev] afp-2016-1 branch

Since the Isabelle2016-1 release is approaching, we will be preparing the new afp-2016-1 release branch as well. If there are any urgent changes or updates to afp-devel that still need to go into afp-2016-1, please let me know. I am planning to fork off the branch in two days. Changes after

Re: [isabelle-dev] isabelle-dev repository status

It sounds like the time for the AFP release fork has now come as well. I’m in Garching Tue+Thu afternoon and could do that fork this week. Cheers, Gerwin > On 27 Nov 2016, at 9:05 PM, Makarius wrote: > > In Isabelle/1c0b93961cb1 I have merged the isabelle-release

Re: [isabelle-dev] Towards the release

That makes sense. Cheers, Gerwin > On 27 Oct 2016, at 00:25, Makarius wrote: > > On 26/10/16 11:58, Makarius wrote: > >> In the past we've had particularly enthusiastic Mac system >> administration at TUM, but I don't see that at the moment. So I am >> reluctant to

Re: [isabelle-dev] Towards the release

I’m planning to switch over to Sierra this week, and can hopefully report back next week on any issues with our l4v proofs, AFP, and isabelle itself. Do we know who is administering macbroy30 and macbroy2? It think it would make sense to switch them over to 10.11 and 10.12 (if the hardware is