[isabelle-dev] Isabelle repository broken
In current 7ff7fdfbb9a0 there is this breakdown: HOL-Quickcheck_Examples FAILED *** No specification for Abs_filter *** At command quickcheck (line 150 of ~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy) *** No specification for Abs_filter *** At command quickcheck (line 145 of ~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy) Since there is no way around a full isabelle build -a before pushing anything, such incidents can't happen, at least in theory. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle repository broken
Sorry this was my fault. isabelle build -a does not guarantee that the current changes are actually committed... BTW, can the predicate_compiler setup s.t. typedefs are ignored automatically? - Johannes Am Montag, den 13.04.2015, 11:28 +0200 schrieb Makarius: In current 7ff7fdfbb9a0 there is this breakdown: HOL-Quickcheck_Examples FAILED *** No specification for Abs_filter *** At command quickcheck (line 150 of ~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy) *** No specification for Abs_filter *** At command quickcheck (line 145 of ~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy) Since there is no way around a full isabelle build -a before pushing anything, such incidents can't happen, at least in theory. 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] datatype takes minutes, but timing panel shows 10s
Hi Andreas, I've investigated this a bit and the slowdown happens in the code plugin in the instantiation of the equal type class (i.e. datatype (plugins del: code) is more precise than the advice below). The number of theorems proved there is quadratic (8000 in your case). But it is still not hopeless: those 8000 theorems are proved one after each other calling Goal.prove for each of them. It is much faster to form the (balanced) conjunction, call Goal.prove (which does among other things type checking) once, and then destroy the conjunction. I'm currently testing this on testboard (http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010). Cheers, Dmitriy On 09.04.2015 16:11, Andreas Lochbihler wrote: Hi Dmitriy and Jasmin, Thanks for the hint with plugins. That really speeds things up. I also suspect that the timing panel does not include the forked proof tactics. Cheers, Andreas On 09/04/15 15:55, Dmitriy Traytel wrote: Hi Andreas, rather than going dirty, try: datatype (plugins only:) family ... It seems that here we are lucky and the slowdown is caused by one of the plugins. (We'll investigate which one.) Cheers, Dmitriy PS: Your datatype reminded me of another one, which allows (or allowed) proving False in a different theorem prover ;-) https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html On 09.04.2015 15:44, Jasmin Blanchette wrote: Hi Andreas, In Isabelle2014, processing this datatype declaration takes about one minute. So what has happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.) Thanks for your report. What happened in between is that we generate more theorems. I suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the number of constructors. As for the timing panel, I suspect it does not take into consideration the time spent in tactics with multithreading on, but I’m not an expert there. We’ll look into this. You could try “quick_and_dirty” around that particular datatype to make things more tolerable in the meantime. Cheers, Jasmin ___ 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] Mira still alive?
This raises the questions whether somebody is still seriously relying on mira or whether it it time to admit that this approach has failed after some initial enthusiasm in 2010/2011. I would still appreciate a less ambitious continuous integration testing environment for Isabelle etc. using existing platforms, e.g . Jenkins. Some time ago I performed some trials with Jenkins to determine which parts of the current workflow can still be supported: * the nightly builds are trivial to model in Jenkins * testboard might need some work, but it is feasible * all my attempts at getting Jenkins to properly version (as in: store changes in a Git or Mercurial repository) failed because the plugins which promise to do this are either outdated, broken or both * it natively supports LDAP-based authentication via web which makes it easy to make changes in the build configuration * building on multiple hosts in parallel is simple and requires very little setup apart from a working SSH connection The major pain point with Jenkins is ensuring security: If we run this service ourselves* _and_ it should be accessible from the Internet (not just from TUM's internal network), it needs continued attention, both for the operating system and Jenkins. Jenkins releases happen very frequently (~ once a week). This wasn't a problem with Mira previously, because the attack surface is much smaller. (AFAIK the web interface is read-only.) The good news is that administrating a Jenkins server does not require root access, which means we might be able let our local sysadmins manage the server. I'll try to investigate whether they have the resources for that. Cheers Lars * The other option – a hosted Jenkins instance – likely won't work for us, because the available machines are not beefy enough (e.g. CloudBees offers VMs with a measly 8 GB RAM, as compared to our own lxbroy10 which has 128 GB). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
