Re: [isabelle-dev] An experience report on the testboard

2016-07-02 Thread Lars Hupel 
Hi Florian,

thanks for your feedback! Commenting in some more detail will take me
some time, but for now a quick reply:

> 1. Changesets to dist and AFP exist as hg patches.

This is currently not implemented. Isabelle testboard will always use
AFP devel and vice versa. It is not possible to test Isabelle testboard
and AFP testboard together.

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

[isabelle-dev] Considered harmful: surj

2016-07-02 Thread Florian Haftmann 
Hi all,

since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
UNIV›. This is a little bit unfortunate since an ordinary equation is
just hidden in output that way, resulting in lots of casual confusion. I
would suggest to turn ‹surj› into a mere input abbreviation, similar to
‹trivial_limit› which also covers an equality. This may also open the
possibility to re-introduce ‹surj_on f A› as in input abbreviation for
‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange
assymmetry wrt. inj(_on), bij(_betw).

Cheers,
Florian

-- 

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



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

[isabelle-dev] {0::nat..<n} = {..<n}

2016-07-02 Thread Florian Haftmann 
Hi all,

obviously on natural numbers ‹{0..

[isabelle-dev] An experience report on the testboard

2016-07-02 Thread Florian Haftmann 
Hi all,

I have started to use the testboard and want to excite feedback on my
workflow, as well as hint to certain inconveniences in the current setup.

1. Changesets to dist and AFP exist as hg patches.

2. In both repositories:
hg push_to_testboard
where »push_to_testboard« according to .hgrc is defined as
alias for
»!{ "${HG}" push -f testboard && "${HG}" phase --force --draft; }«

3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
await new build run to be scheduled.

4. Check that newly emerging build and compare the hash ids according to
http://isabelle.in.tum.de/repos/testboard/summary and
https://bitbucket.org/isa-afp/afp-testboard/commits/all

Here I encountered two problems:
* Even if pushes occur in close proximity, there is a chance that they
are not matched in that particular build.
* To resolve the situation, I did qpop and qpush, this creating patches
with different hash ids. But pushing that did not trigger a new run.
Don't know what's exactly going on here…
A disadvantage is that you have to click a lot to find out the hash id
in the distribution view. I guess that could be easily resolved by a
suitable configuration, or hosting the distribution testboard repository
in the same hosting environment as the AFP testboard repository.

5. Then repeatedly check the URI of the build until results are available.

An inherent weakness of the testboard approach is that whenever you
gradually improve your changesets you to rebuild ab initio. But the
building times are compact enough that this shouldn't be too big a problem.

Cheers,
Florian


-- 

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