With the latest 2.2.X version of cadical, lean4's test suite fails.
This can be mitigated by packaging the old version as cadical-2.1.
* gnu/packages/maths.scm (cadical-2.1): New variable.
* gnu/packages/lean.scm (lean4)[inputs]: Replace cadical with cadical-2.1.
Change-Id: Id5e4a06266e0688454040caf0766bf8d769bbd10
Signed-off-by: Liliana Marie Prikler <liliana.prikler@gmail.com>
The lean4 package currently builds and installs without a visible
failure, but fails to effectvely provide its output, such as the "lean"
binary.
This is due to the install phase of the derivation failing silently as
it tries to access a bash shell using an absolute path that expects an
FHS compliant system.
To fix the issue, the relevant path in "src/stdlib.make.in", which is
used during the install phase of the of the project, is now patched out
by the package definition.
* gnu/packages/lean.scm (lean4):
[arguments] Add substitution for FHS path in "src/stdlib.make.in"
Change-Id: Ib3db9ce1fbb46175130f9b46c58c55cd65a4a1ae
Signed-off-by: Sharlatan Hellseher <sharlatanus@gmail.com>
* gnu/packages/lean.scm (lean): Update to 3.51.1.
[home-page]: Use new home page.
[arguments]<#:phases>: Remove stale phase 'patch-tests-shebangs'.
[inputs]: Remove bash-minimal.
Change-Id: Ib90a124b4a6b06fb30223ad4b9254249e56dd086
Signed-off-by: Ludovic Courtès <ludo@gnu.org>
* gnu/packages/lean.scm (lean): Update to 3.41.0.
[phases]: Remove trailing #t.
[tests?] Set to #false when cross-compiling.
[inputs]: Add bash-minimal.
Co-authored-by: Maxime Devos <maximedevos@telenet.be>
* gnu/packages/lean.scm (lean)[arguments]: Individual test cases are currently
failing for 32-bit architectures. Disable them temporarily pending further
investigation as to resolution.