The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

The regression tests are run every night as far as I know, the results of the last bench (done during the night here in France) are described here for trunk version: http://www.lix.polytechnique.fr/coq/bench/coqbench.cgi?version=trunk . There is no nightly/weekly builds but if you take the git version of, say, 3am (GMT) it should correspond to the last bench. You have to compile it by yourself.

But again if you use third-party libraries you may have troubles.

Hope this helps.

P.

Le mar. 20 janv. 2015 à 09:16, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Pierre,

Coq comes with a test suite but I don't know if every integration of code into Git is tested prior to integration. My question was if there are e.g. weekly builds which are known to pass the regression tests.  If so, I would prefer to use such a weekly build rather than the trunk version. Of cause I could also make a script which pulls the latest version once a week, runs the test suite, and if successful I update to it.

Best regards,

Michael

-----Original Message-----
From: coq-club-request AT inria.fr [mailto:coq-club-request@inria.fr] On Behalf Of Pierre Courtieu
Sent: Monday, January 19, 2015 6:05 PM
To: Coq Club
Subject: Re: [Coq-Club] Simplification of terms generated with tactics

Hi, I am not sure what you call regression tests. There are regression tests in coq but there are a number of incompatibilities bteween 8.4 and trunk that are on purpose (new features, bugfixes). So when you switch to trunk you have to upgrade your code. And most third-party libraries are upgraded only after official releases (beta releases at best).

The only library that follow the trunk day by day is the standard library. User contribs
(http://www.lix.polytechnique.fr/coq/pylons/contribs/list) are also maintained most of the time, although they are often outdated with respect to there original version.


Best regards,
Pierre

2015-01-19 17:35 GMT+01:00 Jonathan Leivent <jonikelee AT gmail.com>:
>
> On 01/19/2015 10:58 AM, Soegtrop, Michael wrote:
>>
>> Dear Jonathan,
>>
>> It looks like I should give 8.5 a try and see if the other things I
>> need work out of the box.  Are there 8.5 prerelease versions which
>> passed a reasonable set of regression test or should I just use the
>> git trunk version?
>>
>> Best regards,
>>
>> Michael
>
>
> I am using a recent trunk version, and I tend to keep it close to the
> latest trunk version so I can see any changes in behavior before
> becoming too dependent on them.  I have only on rare occasion fetched
> a trunk version and found it failed tests so badly as to be unusable -
> mostly it would fail to build - but the Coq developers do a very good
> job of making sure any such blocking bugs are fixed very quickly once
> they are reported.  Note that you get a regression test suite with Coq
> - in the test-suite subdirectory - that you can check yourself.
>
> At this point, I think the Coq developers are very close to releasing
> the first 8.5 beta, but don't know how close.  However, probably
> because of this, the trunk isn't undergoing much change lately that
> would threaten stability.
>
> So, if you can't wait for 8.5 to be released, and would like to
> experiment with it, I would suggest using a trunk version as anything
> you do with it will probably continue to work on the released 8.5.
>
> -- Jonathan
>