Re: [isabelle-dev] Build NEWS

2016-07-17 Thread Lars Hupel
> Anyway, there's now a reboot of these pages available at: > > > > Note that this is a preview: The status is still [skipped] everywhere > and most download links don't work. This will be fixed some time this week. This is now done, see for example

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Lars Hupel
>> I’m sure there are quite some papers which reference the /devel >> entries. > > I should hope not - they make no sense to cite, because their whole > purpose is to change on a daily basis. I'm with Gerwin here. In fact, the devel pages clearly state: "Please refer to release versions only in

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Andreas Lochbihler
For published versions, there probably should not be any /devel-entries links. But for papers under submission, people may have updated their AFP entries and want the reviewers to access the updated material. At least that is what I used to do for many ITP submissions. So it might be good to

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Gerwin Klein
On 11 Jul 2016, at 16:03, Johannes Hölzl wrote: > > Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel: >> Dear AFP developers, >> >> some of you may have noticed that the "AFP devel" pages have not been >> updated since April. This is partly my fault because I migrated

Re: [isabelle-dev] Build NEWS

2016-07-11 Thread Johannes Hölzl
Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel: > Dear AFP developers, > > some of you may have noticed that the "AFP devel" pages have not been > updated since April. This is partly my fault because I migrated the > infrastructure and partly not my fault because the scripts to

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Ondřej Kunčar
On 06/13/2016 07:48 PM, Lars Hupel wrote: * AFAIS, pushing to the Isabelle testboard still requires local access > rights at TUM. Are there any fundamental impediments to lift this > restriction? Yes. I have been arguing that we should move the official Isabelle repository to Bitbucket for a

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Lars Hupel
> * The URLs to push to are IMHO best presented using an hgrc excerpt, e.g. > >> [paths] >> testboard = ssh://h...@bitbucket.org/isa-afp/afp-testboard >> >> [alias] >> push_to_testboard = push -f testboard > > That way the risk for accidental pushes is greatly reduced Good idea. > * AFAIS,

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Florian Haftmann
>> * As pointed out by Larry, navigation on the Jenkins pages is a >> pain. I've revamped the status page with helpful links to the build >> outputs of the various jobs and instructions on how to use the >> testboard: >> >> Ah, excellent. Just two

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Lars Hupel
> Is there any consolidated documentation »How to test changesets > before contributing« or the like? I must confess that I don't even > know where to push changesets to, it is somewhere buried in my > mailbox. See my original mail: > * As pointed out by Larry, navigation on the Jenkins pages

Re: [isabelle-dev] Build NEWS

2016-06-13 Thread Florian Haftmann
Is there any consolidated documentation »How to test changesets before contributing« or the like? I must confess that I don't even know where to push changesets to, it is somewhere buried in my mailbox. Thanks a lot, Florian Am 13.06.2016 um 08:55 schrieb Lars Hupel: > Dear Isabelle

Re: [isabelle-dev] Build NEWS

2016-04-20 Thread Lars Hupel
> * I'm still working on getting the build to be more stable (i.e., get rid > of spurious failures). I've had a productive discussion with Gerwin how to > achieve that. Looks like this has been achieved. I haven't seen any spurious failures again. Also, build logs are now archived. If you pushed

Re: [isabelle-dev] Build NEWS

2016-04-17 Thread Lars Hupel
> Maybe this can be simplified further. The "slow" group in the main > Isabelle repository is now rather pointless, even counterproductive. > HOL-Proofs and its subsessions has become relatively fast compared to > other bulky sessions. > > E.g. Isabelle/65f279853449 on 12 cores with 6 threads per

Re: [isabelle-dev] Build NEWS

2016-04-17 Thread Makarius
On Sat, 16 Apr 2016, Lars Hupel wrote: * I have eliminated the last occurrence of ISABELLE_FULL_TEST in the known Isabelle universe. Flyspeck_Tame used it to determine whether full computations should be carried out. It does that now by default, which takes about 7 hours (!) on a regular

[isabelle-dev] Build NEWS

2016-04-16 Thread Lars Hupel
Dear list, I'd like to summarize the recent progress in the build infrastructure. * I'm still working on getting the build to be more stable (i.e., get rid of spurious failures). I've had a productive discussion with Gerwin how to achieve that. * Once that is done, the build mails will get