Activity for Guillaume Verdier
-
Guillaume Verdier modified ticket #42
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
1 >