Atomicity Decomposition Plug-in Install failed
One of the developers of the plug-in confirmed that it is unmaintained and does not work with recent Rodin releases.
User-defined keyboard mappings
atelierb installation fails
Here is a different, probably simpler, procedure to run the Intel version of Rodin (which can use AtelierB provers) on macs with Apple Silicon processors: 1. download https://github.com/adoptium/temurin17-binaries/releases/download/jdk-17.0.11%2B9/OpenJDK17U-jre_x64_mac_hotspot_17.0.11_9.pkg (it's a Java 17 runtime for Intel) 2. install it by double-clicking it; the Java runtime is installed in /Library/Java/JavaVirtualMachines/temurin-17.jre 3. find the downloaded Rodin.app and modify Rodin.app/Contents/Eclipse/rodin.ini:...
Keep information about basic constructors
Issues with DatatypeHelper.computeId
Add missing @ProverRule annotation for DEF_EXPN_STEP
Put children WDs first in WD of extensions
Update composite sites: use https and archive old versions
Synchronize access to global datatype registry
Small cleanup and optimisation of extension unicity checker
Inline two trivial private methods that were only used in one place
Use set instead of list to check symbol duplication
Remove old update sites that do not work anymore
Thanks for your detailed reports. This is a known issue with the program checking the provers at startup (the first run of external programs can be much slower than the next ones due to various causes — the OS checking the binary, caches being empty, Rosetta doing some translation, and so on — so this first run timeouts and causes the error message, but there is nothing actually wrong). The AtelierB provers should still work without any issue in actual proofs.
I have an older Intel mac, but from what I've been told, you have to install an x86 version of Java and then you should be able to run an x86 Rodin. However, someone else reported by email that the installation of AtelierB provers also fails with the x86 version of Rodin 3.9-rc1. We are investigating it. If you want a stable and complete version of Rodin quickly, installing the x86 version of Rodin 3.8 is your safest bet.
Do you use the x86 version of Rodin through Rosetta? AtelierB provers are only distributed as x86 binaries, so they can't be installed on an ARM/Apple Silicon build of Rodin.
Update URLs of update sites for ProB and Camille
Eclipse now requires to use https for update sites: update URLs
New reasoners on inductive types
The suggested rules have either been directly implemented or are now easily provable. The changes have been merged in commit [160fb8].
Add update site for archive of old versions of plug-ins
Cleanup IRodinProject
Cleanup IRodinFile
Depreciate IRodinFile.findElements()
Remove unused API filters
Prepare Rodin 3.9 RC1
Increment version of parent in all pom.xml files, plugins and features to 3.9
Disabling automatic workspace updating
Correcting some tests to take into account the apparition of the folder .settings when creating a new project
updating all feature.properties, about.properties, splash files
Minor increment of some plugin versions after upgrading the Java version
Upgrading the Required Java version to JavaSE-17
Fix FR #396: New reasoners on inductive types
Add auto rewrite rule for membership of constructor to datatype
Add auto rewrite rule for equality of datatypes with set parameters
Add more tests on existing auto rewrite rules for datatypes
Better simplification of identity
The requested rules have been implemented in commit [8b2820].
User provided names for fresh variables in reasoners
It has been implemented and merged in commits [0dec3b] (for ae), [35868a] (for allI), [28a73c] (for dt dc) and [345499] (for exF).
Cleanup test names in auto rewriter L3 tests
Fix FR #368: Better simplification of identity
Update example test class to use more modern test methods
Simplify and optimise true goal reasoners
Remove unused internal class OnePointFilterUtils
Fix FR #403: User provided names for fresh variables in exF
Small cleanup in ExF (simplify test and remove extra line breaks)
Allow users to provide the names to use in ExF
Allow sub-classes of ForwardInfReasoner to extend more things
Use more modern methods to test ExF
Fix FR #403: User provided names for fresh variables in dt dc
Allow users to provide the names to use in datatype distinct case
Allow sub-classes of PredicatePositionReasoner to extend serialization
Ensure that test sequents are parsed with the right factory
Use a more modern method to test positions of DTDistinctCase
Fix FR #403: User provided names for fresh variables in allI
Allow users to provide the names to use in allI
Small cleanups in AllI (static import, indentation, ...)
Use more modern methods to test AllI
Simplify string generation for AllI proof rule display
Fix typo in AllI documentation
Miscellaneous fixes and cleanups in the seqprover
Add Cloneable interface to ReplayHints
Remove TODO for which there is nothing to do
Rename attribute of ReplayHints as suggested in TODO
Remove proofSimplifier package
Remove TODO that should not be implemented
Remove TODO that should not be implemented
Fix FR #403: User provided names for fresh variables in ae
Fix variable name in SingleExprInput
Allow users to provide the name to use in ae
Implement TODO in tests of AbstrExpr
Remove irrelevant comment
Use more modern methods to test AbstrExpr
Autorewriter generates invalid proof rule
It has been fixed and merged in commit [67fd5a].
Fix bug #829: Autorewriter generates invalid proof rule
Fix tests that were using serialized proofs with auto rewrites
Fix another bug related to bound identifiers
Fix bug #829: Autorewriter generates invalid proof rule
Rewrite rule for recursive exponentiation
This rule has been implemented and merged in commit [53cd8c].
Miscellaneous fixes to UI's extension parser
Factor out common code when computing items of a toolbar
Refactor extension parser and toolbar info according to several FIXMEs
Cleanup UI's extension parser
Cleanup UI's extension parser
Clarify documentation of genFullSeq
Remove old, unused code in keyboard UI that was noted to be broken
Make explicit calls to the post tactic interruptible
Ensure that adequate method is always used to apply tactics
Remove old tactic application method that is not used anymore
Simplify dynamic dropdown manager implementation
Use a progress dialog for instantiation post tactic
Use a progress dialog if needed for tactics run through PredicateRow
Simplify tactic application in predicate row
Fix FR #398: Rewrite rule for recursive exponentiation
Simplify and optimize generic getPositions() for manual inferences