Re: [isabelle-dev] Build NEWS

[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

  


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

Re: [isabelle-dev] Build NEWS

[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 citations."

If you need to refer to some current development for any purposes, you
should really be using the Mercurial id, just as we do for the Isabelle
repository.

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

Re: [isabelle-dev] Build NEWS

[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 keep the /devel-entries URLs alive at least for some 
transition period.


Andreas

On 11/07/16 08:09, Gerwin Klein wrote:

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 the
infrastructure and partly not my fault because the scripts to produce
these pages make a lot of assumptions about the infrastructure :-)

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.

As soon as that's done, the old links ("/devel-entries" and the like)
will go offline.


Can't we just let the /devel-entries redirect to http://devel. ?


That would not be too hard, but



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.

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
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] Build NEWS

[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 the
>> infrastructure and partly not my fault because the scripts to produce
>> these pages make a lot of assumptions about the infrastructure :-)
>>
>> 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.
>>
>> As soon as that's done, the old links ("/devel-entries" and the like)
>> will go offline.
>
> Can't we just let the /devel-entries redirect to http://devel. ?

That would not be too hard, but


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

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[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 produce
> these pages make a lot of assumptions about the infrastructure :-)
> 
> 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.
> 
> As soon as that's done, the old links ("/devel-entries" and the like)
> will go offline.

Can't we just let the /devel-entries redirect to http://devel. ?  I'm
sure there are quite some papers which reference the /devel entries.

> Cheers
> Lars

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

Re: [isabelle-dev] Build NEWS

[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 while. If you too want this to happen,
please say so loud and clear here, so that my lobbying efforts carry
more weight :-)


As far as I understand it, to solve the problem that Florian mentioned, 
it would be enough to move only the testboard repository to Bitbucket. I 
wouldn't have anything against it.


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

Re: [isabelle-dev] Build NEWS

[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, 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 while. If you too want this to happen,
please say so loud and clear here, so that my lobbying efforts carry
more weight :-)

There are no other alternatives that I'm aware of which allow repository
access based on SSH keys, account setup without bureaucracy, and no
conflation between "repository admin" and "push access" (the latter is
inherent when using Unix groups).

Luckily migrating Mercurial repositories is trivial.


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

Re: [isabelle-dev] Build NEWS

[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 remarks:

* 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

* AFAIS, pushing to the Isabelle testboard still requires local access
rights at TUM.  Are there any fundamental impediments to lift this
restriction?

Cheers,
Florian


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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Build NEWS

[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 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:
> 
>   
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[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 developers,
> 
> this is an update about recent and upcoming changes in the build
> infrastructure.
> 
> * Starting with Isabelle/e0513d6e4916 and AFP/e6727c33 I have moved
> the Jenkins build scripts into the Isabelle and AFP repository (they
> used to reside in a private "admin" repository). Each "build profile" is
> a separate Isabelle tool. In order to not pollute the global tool
> namespace, they are not enabled by default. If you want to run them
> yourself, the necessary setup is:
> 
>   - in your personal etc/settings, add a line to init components from
> "ci-extras" (not just from "main")
>   - register components "$ISABELLE_HOME/Admin/jenkins/build" and
> "$AFP_BASE/jenkins"
> 
> * New build hardware has arrived and will be provisioned over the next
> two weeks. I will start migrating jobs to the new hardware. This will
> bring build time for AFP (excl. "slow") down to about 90 minutes, from
> over 180 minutes before. There will be no more excuse not to use the
> testboard(s) liberally :-)
> 
> * 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:
> 
>   
> 
> Suggestions for additions welcome.
> 
> * The AFP devel pages have not been regenerated in a while. I'm aware of
> this issue. Now that the build scripts are in the AFP repository and old
> afptest has been discontinued, I can start migrating the old
> configuration which generated these pages.
> 
> Cheers
> Lars
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Build NEWS

[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 a changeset which
breaks the build, go to the last job execution, e.g.

  

... and you'll find a list of archived log files directly there.

In the near future, generated documents will also appear there.

Cheers
Lars


PS: I'm working on a small "howto" page which explains how to find the
information you're looking for in Jenkins. For that to be useful, please
tell me what information you'd be usually looking for.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Build NEWS

[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 ML process:
> 
> build -j4 -a
> 0:27:21 elapsed time, 7:13:18 cpu time, factor 15.84

Thanks for that observation. This is now rectified in Isabelle/d0dfdd413a7f.

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

Re: [isabelle-dev] Build NEWS

[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 machine. I have also tagged
  this session with "slow" (like the other huge sessions). If you want
  to test the AFP locally without provoking the heat death of your
  machine, I recommend building with "-X slow".


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 ML process:

build -j4 -a
0:27:21 elapsed time, 7:13:18 cpu time, factor 15.84


build -j4 -a -X slow
0:23:53 elapsed time, 6:02:21 cpu time, factor 15.17

build -j4 -g slow
0:12:23 elapsed time, 0:57:07 cpu time, factor 4.61


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

[isabelle-dev] Build NEWS

[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 switched on again for some
jobs. The code for sending out afptest-style mails is already there and
just needs to be deployed.

* 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 machine. I have also tagged this
session with "slow" (like the other huge sessions). If you want to test
the AFP locally without provoking the heat death of your machine, I
recommend building with "-X slow".

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