Benoit

Bug in the definition soundness check

1

The definition soundness check didn't catch an unsound definition in https://github.com/metamath/set.mm/pull/3339 even though that definition has free setvars in its definiens: ``` $c $. wich $a wff [ x y...

On Debian, I followed the instructions from the paragraph "Building mmj2 with maven" of INSTALL.md up to ``` $ mvn package [INFO] Scanning for projects... [INFO] [INFO] ------------------------------< mmj:mmj2 >------------------------------...

On Debian, I followed the instructions from INSTALL.md up to ``` $ compile/posix_compile find: ‘../lib’: Aucun fichier ou dossier de ce type javac: directory not found: ../classes Usage: javac use...

Some tests are not run when the corresponding file opens other modules

3

Alcotest has a strange (buggy?) behavior when a test file opens a module of the library of the same project. In the example below, `test/dune` indicates that there are two...