longs axioms not displayed correctly
1/ This has apparently been fixed at some point: long axioms can span on several pages. 2/ If a formula is too long and overflows its line, it's possible to insert line breaks in the Rodin editors; they will be carried over by B2Latex.
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