Port details on branch 2024Q2 |
- lean4 Theorem prover and functional language for math (new gen)
- 4.6.0 math =0 4.6.0Version of this port present on the latest quarterly branch.
- Maintainer: yuri@FreeBSD.org
- Port Added: 2024-05-06 08:45:10
- Last Update: 2024-05-06 08:44:40
- Commit Hash: 38ef1b2
- Also Listed In: devel lang
- License: APACHE20
- WWW:
- https://lean-lang.org/
- Description:
- Lean is an open source theorem prover and programming language being developed
at Microsoft Research. Lean aims to bridge the gap between interactive and
automated theorem proving, by situating automated tools and methods in a
framework that supports user interaction and the construction of fully specified
axiomatic proofs. The mathematical components library mathlib for Lean is being
developed at Carnegie Mellon University.
- ¦ ¦ ¦ ¦
- Manual pages:
- FreshPorts has no man page information for this port.
- pkg-plist: as obtained via:
make generate-plist - Dependency lines:
-
- To install the port:
- cd /usr/ports/math/lean4/ && make install clean
- To add the package, run one of these commands:
- pkg install math/lean4
- pkg install lean4
NOTE: If this package has multiple flavors (see below), then use one of them instead of the name specified above.- PKGNAME: lean4
- Flavors: there is no flavor information for this port.
- distinfo:
- TIMESTAMP = 1709183089
SHA256 (leanprover-lean4-v4.6.0_GH0.tar.gz) = 9e90f38c9b55e8accc27f75394db1fcdb58bc4dc22ba99d1232e4921c66ff2af
SIZE (leanprover-lean4-v4.6.0_GH0.tar.gz) = 17532157
No package information for this port in our database- Sometimes this happens. Not all ports have packages.
- Dependencies
- NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
- Build dependencies:
-
- bash : shells/bash
- cmake : devel/cmake-core
- gmake>=4.4.1 : devel/gmake
- python3.9 : lang/python39
- Library dependencies:
-
- libgmp.so : math/gmp
- There are no ports dependent upon this port
Configuration Options:
- No options to configure
- Options name:
- math_lean4
- USES:
- cmake:noninja,testing compiler:c++14-lang gmake python:build
- pkg-message:
- For install:
- ================================================================================
You installed Lean: The Theorem Prover.
(1) Please note that Lean requires /proc to be mounted.
The usual way to do this is to add this line to /etc/fstab:
proc /proc procfs rw 0 0
and then run this command as root:
# mount /proc
(2) You might also want to install mathlibtools (math/mathlibtools) in case
you need to use the mathematical library of Lean.
mathlibtools download this library to user's home directory for further
use by Lean.
================================================================================
- Master Sites:
|
Number of commits found: 1
Commit History - (may be incomplete: for full details, see links to repositories near top of page) |
Commit | Credits | Log message |
4.6.0 06 May 2024 08:44:40 |
Yuri Victorovich (yuri) |
math/lean4: Broken on armv7
Reported by: fallout
(cherry picked from commit 39cc19929dda91e10fd0b92cc16b1f506cb57e2c) |
Number of commits found: 1
|