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

[Gerwin.Klein]

> 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 require some coordination, especially on AFP.
> 
> E.g. one could set a date for the "big sweep" and make one big
> changeset, or one could gradually update entries in an erratic manner.
> 
> You can probably say better if there are problems to be expected between
> the "stable" and "devel" versions of AFP.

I don’t expect too much trouble from this one. It might make sense to try out 
how the conversion goes a few entries first, and then, if that is satisfactory, 
do a big change set for the rest. 

Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 ... from my side there are no uses of 
this quotation remaining that I'd know of

However, (* *) is still very important for informally andquickly commenting 
things out, also in inner syntax!


Peter


 Original Message 
Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?
From: Makarius
To: isabelle-dev
CC:


Over the decades we have accumulated funny quotation forms in Isabelle
syntax that are often hard to explain to new users (also to old users).

In particular, what are the remaining uses of {* ... *}?

It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get rid of it (as well as `alt_string`).


The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

> 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 don't see any remaining applications in Isabelle + AFP. So it looks
> like we can just remove it without further ado.

Confirming that this would also be safe from our side.

Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

> 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, it’s too far away from what the AFP 
is supposed to achieve.

Distributing it as a component together with Isabelle would work, though, I 
think. 

Cheers,
Gerwin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] a question about regulations

[Gerwin.Klein]

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 reproduce the above copyright 
notice, this list of conditions and the following disclaimer in the 
documentation and/or other materials provided with the distribution.

* Neither the name of the University of Cambridge or the Technische
Universitaet Muenchen nor the names of their contributors may be used
to endorse or promote products derived from this software without
specific prior written permission.

This is very permissive.

There are no restrictions for other .thy files, only the usual copyright and 
other IP laws apply. We have commercial contracts that deliver .thy files quite 
routinely.

Cheers,
Gerwin

> On 28 Jun 2018, at 07:55, José Manuel Rodriguez Caballero 
>  wrote:
> 
> Dear Sir or Madam,
> 
>   Motivated by my exchange of experiences with professionals using 
> proof-assistants like Coq for commercial purposes, I would like to ask the 
> following question is: which are the regulations of Isabelle for commercial 
> use? For example, if a software company is interested in selling .thy files 
> to clients, which conditions apply?
> 
> Sincerely yours,
> José M.l Rodriguez Caballero
> Université du Québec à Montréal
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 actually getting 'isabelle afp_build
>> -A' to run through?  I was hoping to find that in
>> /doc/regression-test.md but that merely states the command.
> 
> My command-line usually looks like this:
> 
>  isabelle build -d '$AFP' -a -X slow -j4
> 
> Or:
> 
>  isabelle build -d '$AFP' -a -X very_slow -j4
> 
> You can also use -D '$AFP' (without -a) to address precisely the AFP
> sessions.
> 
> 
>> It appears that I would need to set ML_PLATFORM=x86_64-darwin for the
>> large sessions but then some magic seems to defeat that and builds are
>> still for x86-darwin.
> 
> Instead of editing $ISABELLE_HOME_USER/etc/settings to change
> ML_PLATFORM (which is difficult to get right), I usually edit
> $ISABELLE_HOME_USER/etc/preferences to add:
> 
>  ML_system_64 = true
> 
> Only some "slow" sessions do need x86_64, but some non-slow sessions
> (like HOL-ODE-Numerics) become a bit slow in x86 mode. Almost everything
> else works better in x86 mode, which is the default.
> 
> See also
> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads/index.html
> for typical maximum heap requirements.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 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?

Isabelle2017-RC3 is fairly stable and deserves a proper afp-2017
repository fork.

Having a clear correspondence of isabelle-dev vs. afp-devel and
Isabelle2017 vs. afp-2017 also means that changes to the devel branches
can be again more ambitious.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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?
> 
> Isabelle2017-RC3 is fairly stable and deserves a proper afp-2017
> repository fork.
> 
> Having a clear correspondence of isabelle-dev vs. afp-devel and
> Isabelle2017 vs. afp-2017 also means that changes to the devel branches
> can be again more ambitious.
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2017 release

[Gerwin.Klein]

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, Makarius  wrote:
> 
> We are now past the fork point for the Isabelle2017 release.
> 
> Here is a summary of the status of the Isabelle development process:
> 
>* https://bitbucket.org/isabelle_project/isabelle-release/ is where
>  the final release preparations happen before roll-out in a few
>  weeks.
> 
>  The starting point is
> https://bitbucket.org/isabelle_project/isabelle-release/commits/bcea02893d17
> 
>* http://isabelle.in.tum.de/repos/isabelle is back in post-release
>  mode right now (changeset 435cb8d69e27).  Anything pushed there
>  is for the next release after Isabelle2017.
> 
>* AFP (presently at dfb6f8bc70e3) needs to be understood wrt.
>  isabelle-release at the moment. Gerwin will explain when and how
>  the fork of afp-devel vs. afp-2017 happens.
> 
>* http://isabelle.in.tum.de/devel with the automated testing and
>  snapshot service follows the isabelle-dev repository; I've
>  refrained from forking that as well to keep the long term test
>  results in a linear form.
> 
>* isabelle-users is the place to discuss Isabelle2017-RC versions.
> 
>* isabelle-dev is the place to discuss ongoing post-release
>  development.
> 
> 
> The isabelle-release repository has no public push access. Any changes
> that are relevant for the release need to be sent to me via email
> (produced by "hg export" or "hg bundle"). Changesets need to be
> prepared from a current state of isabelle-release, not the ongoing
> post-release development, and applied to only one of the two repository
> branches.
> 
> Changes to the actual code base should be limited to really important
> things.
> 
> During the forked state of the two repositories, big upheaveals on the
> isabelle-dev repository should be avoided, so that the isabelle-release
> branch can be merged back cleanly after some weeks; but it is
> better to publish changes now than to stockpile them for a long time.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 looking at the Flyspeck_Tame entry in the AFP today.  The
> current version of proofs built in Isabelle 2016 in a few minutes.
> But there is more to this development than checking the proofs.  There
> are "Proofs by evaluation using generated code" that are only executed
> if ISABELLE_FULL_TEST=true.  These proofs by evaluation take several
> hours to run.
> 
> I wonder if these proofs by evaluation are checked when the AFP is
> brought up-to-date with a new release of Isabelle?  Similarly, do
> other AFP entries have parts that may not be getting checked with new
> releases.
> 
> Thanks for any info.
> 
> --Randy
> 
> On Wed, Nov 30, 2016 at 11:46 AM,   wrote:
>> 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 wrote:
>>> 
>>> 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 that will not make it into the release.
>>> 
>>> Cheers,
>>> Gerwin
>>> 
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
>> 
>> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 wrote:
> 
> 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 that will not make it into the release.
> 
> Cheers,
> Gerwin
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] afp-2016-1 branch

[Gerwin.Klein]

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 that will not make it into the release.

Cheers,
Gerwin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Gerwin.Klein]

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 repository
> back into isabelle-dev, this means that consolidations of release
> candidates are effective on the post-release branch.
> 
> Semantically, we have still a fork of both repositories, until the final
> release of Isabelle2016-1 (which should happen within the next 2 weeks).
> 
> The status of AFP is still unclear to me. The AFP editors need to come
> up with a plan how to proceed.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Gerwin.Klein]

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 change a running system, especially macbroy2, which is very
>> important for the Isabelle administration and release process.
>> 
>> After the release, we can probably discontinue Mountain Lion, and update
>> macbroy30 to El Capitan or Sierra.  Both macbroy30 and macbroy31 are
>> MacBookPro6,2 from Mid 2010, so it looks like Sierra still works, but
>> that might be also the latest possible version.
> 
> I have had a chat with the system administration at TUM. We can keep up
> the status quo with some minor updates, but not much more.
> 
> So the present plan is this:
> 
> * After the release of Isabelle2016-1 (December 2016) we discontinue
> support for 10.8 Mountain Lion and update macbroy30 to 10.12 Sierra
> (probably the ultimate version that is possible on this hardware).
> 
> * After one more release cycle by Apple (2017?) we discontinue support
> for 10.9 Mavericks and update macbroy2 to 10.11 El Capitan (definitely
> the ultimate version that is possible on this hardware).
> 
> 
> This means we hold up the standard of approx. 4 versions of Apple's OS,
> whatever its name might be next year.
> 
> 
>   Makarius
> 
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the release

[Gerwin.Klein]

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 still 
supported).

Cheers,
Gerwin

> On 26.10.2016, at 04:39, Makarius  wrote:
> 
> On 25/10/16 14:29, Jasmin Blanchette wrote:
>> 
>>> The Windows platform is a bit strange, but there are usually many ways
>>> to get things through eventually.
>> 
>> Simon has found a way to avoid "ocamlbuild". It looks like we'll be able to 
>> have the three binaries in place before the branch. Nonetheless, Nunchaku 
>> will remain labeled as "experimental", for a variety of reasons, and will 
>> not be properly documented.
> 
> Great.
> 
> Note that the updated Isabelle PLATFORMS file is here:
> http://isabelle.in.tum.de/repos/isabelle/file/3f4a86c9d2b5/Admin/PLATFORMS#l25
> 
> I have bumped the Linux baseline to Ubuntu 12.04 recently. Cygwin is
> also updated to 2.6 -- last time I somehow missed the change of the
> numbering scheme, so we were lagging behind.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev