package rocq-native

  1. Overview
  2. No Docs
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:

  1. you might face with issues installing this package flag under macOS, see https://github.com/coq/coq/issues/11178.
  2. 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).
  3. 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)

  1. coq-native
OCaml

Innovation. Community. Security.