diff options
| author | Emilio Jesus Gallego Arias | 2020-05-15 13:38:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-15 13:38:12 +0200 |
| commit | bcfb5f2cab54d0eb88ed57911b77c05d2b916431 (patch) | |
| tree | 1ca88bdd7fbd412386a2e0b4041f1929c9b55a75 | |
| parent | 959254ccd5c895782286dfb1d2c731e143e37d00 (diff) | |
| parent | 5383050ccdaca3f1b97e06bb782e5704231e9cdb (diff) | |
Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: ppedrot
| -rw-r--r-- | INSTALL.md | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/INSTALL.md b/INSTALL.md index 2397f2c5c2..c44c3dde7d 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -77,3 +77,20 @@ Please see [INSTALL.make.md](dev/doc/INSTALL.make.md) for build and installation instructions using `make`. If you wish to experiment with the Dune-based system see the [dune guide for developers](dev/doc/build-system.dune.md). + +Run-time dependencies of native compilation +------------------------------------------- + +The OCaml compiler and findlib are build-time dependencies, but also +run-time dependencies if you wish to use the native compiler. + +OCaml toolchain advisory +------------------------ + +When loading plugins or `vo` files, you should make sure that these +were compiled with the same OCaml setup (version, flags, +dependencies...) as Coq. Distribution of pre-compiled plugins and +`.vo` files is only possible if users are guaranteed to have the same +Coq version compiled with the same OCaml toolchain. An OCaml setup +mismatch is the most probable cause for an `Error while loading ...: +implementation mismatch on ...`. |