Make `(mode native)` configurable

erikmd commented 3 years ago

Summary

This PR is a follow-up of a suggestion by @proux01, which should simplify the packaging of multinomials in Nix (as well as in opam for the upcoming release): it adds an optional CLI arg to ./configure, and don't query coq --version anymore.

To ensure that the CLI parsing is robust, I automatically generated that code using Argbash.

Commit-message details

Make (mode native) configurable

So we can do:

./configure --native-compiler yes
./configure --native-compiler no
./configure # now implying no native-compiler if coq = 8.12.x

As a result, the script is simpler: it needs not check coq's version. Further, it becomes easier to package multinomials in Nix (and opam).

TL;DR:

if Coq ≥ 8.13, it suffices to run ./configure to auto-detect (then enable) coq-native precompilation in Multinomials;
If 8.12.1 ≤ Coq < 8.13, the package manager should run either ./configure -native-compiler no or ./configure -native-compiler yes if coq-native support is expected;
If Coq < 8.12.1, (mode native) being not supported by dune to date, one should just run ./configure (or equivalently, ./configure -native-compiler no).

Cc @CohenCyril @strub @proux01 @ejgallego

proux01 commented 3 years ago

Thanks!

proux01 commented 3 years ago

@erikmd guess what? this is wrong again with nix (thus breaking mathcomp CI):

configuring
patching script interpreter paths in configure
configure: interpreter directive changed from "#!/usr/bin/env bash" to "/nix/store/wadmyilr414n7bimxysbny876i2vlm5r-bash-5.1-p8/bin/bash"
configure flags: --prefix=/nix/store/k03r7h8ii8rwh08hqwncqp6vbprxz9vs-coq8.12-mathcompdev-multinomials-dev
configure script for SsrMultinomials
Usage: ./configure [--native-compiler <arg>] [-h|--help]
        --native-compiler: Pre-compile .coq-native/* files (yes|no)
        -h, --help: Prints help
FATAL ERROR: Got an unexpected argument '--prefix=/nix/store/k03r7h8ii8rwh08hqwncqp6vbprxz9vs-coq8.12-mathcompdev-multinomials-dev'

could you please add a prefix argument with just a warning telling it is ignored? (that's the easiest fix I can think of)

math-comp / multinomials