rocq-nativeversion Documentation on ocaml.org
Package flag enabling rocq's native-compiler flag
This package acts as a package flag for the ambient switch, taken into account by rocq (and possibly any rocq library) to enable native_compute at configure time, triggering the installation of .coq-native/* files for the rocq libraries.
This implements item 1 of CEP #48 https://github.com/coq/ceps/pull/48.
Remarks:
- you might face with issues installing this package flag under macOS, see https://github.com/coq/coq/issues/11178.
- this package is not intended to be used as a dependency of other packages (notably as installing or uninstalling this package may trigger a rebuild of all rocq packages in the ambient switch).
- the option set by this package will be automatically propagated to rocq compile.
| Author | The Rocq development team, INRIA, CNRS, and contributors |
|---|---|
| License | LGPL-2.1-only |
| Published | |
| Homepage | https://rocq-prover.org/ |
| Issue Tracker | https://github.com/rocq-prover/rocq/issues |
| Maintainer | The Rocq development team <rocq+rocq-development@discoursemail.com> |
| Available | arch = "x86_32" | arch = "x86_64" |
| Conflicts |
|
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/rocq-native/rocq-native.2/opam |
Required by
Optionally used by
