package rocq-native
Package flag enabling rocq's native-compiler flag
Install
Dune Dependency
Authors
Maintainers
Description
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.
Published: 12 Jan 2025
Dependencies
None
Dev Dependencies
None
Used by (1)
Conflicts (2)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page