[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 19 Apr 2020 14:43:53 +0200*References*: <7e0fc5aa-f0c0-4f74-807b-bf0d5a114261@googlegroups.com> <363ADD28-A551-4B86-9771-2156D94EDFBF@gmail.com> <0cdf0ab6-f6a5-49dd-8292-ca15db5a01d8@googlegroups.com>

Hello again Nicholas, I don't think any proof assistant promises backward compatibility because that would severely restrict change. In this particular case, the issue moreover appears to have been caused by changes in automatic back-end provers that are not under our control. The mechanism that Isabelle/HOL has adopted with the Archive of Formal Proofs [1] is to collect major proof developments and run regression tests with every new release of the prover. When proofs fail, the Isabelle implementors assess whether they consider the change to be overall positive or if it breaks too many developments. In case the change is retained, maintainers of the collection (and/or the original author) fix the failing proofs so that they are kept up to date with new Isabelle releases. For TLAPS, we do not yet have a critical mass of proofs but some day we may wish to implement a similar policy. Regards, Stephan [1] https://www.isa-afp.org
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8C38ED76-9757-4097-A957-9129459DAC75%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)***From:*'Nicholas Fiorentini' via tlaplus

**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)***From:*Stephan Merz

**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)***From:*'Nicholas Fiorentini' via tlaplus

- Prev by Date:
**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Next by Date:
**Re: [tlaplus] How do you list possible next steps?** - Previous by thread:
**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Next by thread:
**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Index(es):