Ssreflect Users Discussion List

[Georges Gonthier <>]

   Dear Stéphane,

  I believe you already received a private answer to some of your concerns, 
but since you chose to air your issues on the ssreflect users list, I believe 
I should also provide a public answer, if only to give the ssreflect users a 
heads up on what's coming their way.
  We actually have been hard at work on the ssreflect plug-in ever since Coq 
8.3 finalized. That effort is very near completion: there are only a few 
days' work needed on the actual code, the release documentation (Changes 
file, etc) to write, so we do plan to be able to announce ssreflect 1.3 this 
March. This has been substantial work by Enrico Tassi, involving 
reengineering several of the basic algorithms, and adding about a dozen new 
features inspired by our almost 5 years of experience with the language 
(which had not changed much in the meantime). Enrico deserves much credit for 
doing all of this in record time: it took us 9 months to follow up on Coq 
8.1, 6 to do so on Coq 8.2, and we're now down to 3, so there has been some 
improvement...
  As probably many other users on this list, I very much appreciate your hard 
work in creating Coq and Ssreflect distributions, and understand your 
frustration at not being able to do an ssreflect package at the same time. 
But I do insist at doing things somewhat properly and having consistent 
releases. And I can't divert too many of our limited resources from our main 
scientific goal -- developing advanced mathematical libraries -- to tinkering 
with the underlying proof system.
  Concerning the coq-contribs gforge repository you mention, and which all 
members of this list are perhaps not aware of, I would like to stress that 
despite its name it is not an archive of external contributions, but a joint 
regression suite for the Coq internal and external developers. We try to push 
material in that repository eagerly so that both internal Coq developers and 
us learn about portability issues as early as possible. We have hit race 
conditions where Coq developers broke a Coq feature while we started using it 
in the library, and then had to backtrack and were unable to materialize the 
problem in the contrib (one particular problem - inconsistent constant 
expansion in the interpretation of elim .. using - persists in the final 8.3 
release).
  The bottom line is, although the coq contribs does some idea of the 
advancement of our work, it is neither a release candidate nor necessarily 
representative of the latest state and direction of the ssreflect library. It 
can fall out of sync when either the Coq devs or us need to push larger 
changes (as is the case now for the trunk contrib, which you unfortunately 
have had to patch because it has not been fixed by the Coq dev that broke 
it). So, third parties should realize they can only use the contrib at their 
risks and perils.
  Bottom line, we do remain committed to maintaining and improving the 
ssreflect plug-in and libraries -- after all it is our main development tool. 
We do expect to announce the ssreflect 1.3 release Real Soon Now, and in the 
meantime thank you (especially) and all our users for their support and 
patience.

  Cheers,

Georges Gonthier

-----Original Message-----
From: Stéphane Glondu [] 
Sent: 22 February 2011 10:39
To: 
Cc: Coqdev
Subject: [coqdev] Ssreflect with Coq 8.3

Hello,

Currently, we are in the strange situation where ssreflect in the 
contribs has been kept synchronized with upstream development 
repository, and works with 8.3, and the latest release of ssreflect 
doesn't work with 8.3.

Coq 8.3 has been released more than 3 months ago, and with a working 
ssreflect contrib. Still, no new release of ssreflect working with Coq 
8.3 has been done. This is very disappointing for me, because I maintain 
contribs (in general, not only ssreflect) in a working state, but this 
work cannot be used in a production environment with the current 
ssreflect/contrib interaction.

The current situation is unacceptable. I think only the latest release 
should be in the contribs. Ssreflect developpers should stop updating 
automatically the contribs repository the way they do. They should make 
releases more often if they want their code to be ported by Coq developers.


Cheers,

-- 
Stéphane