diff options
| author | Théo Zimmermann | 2020-05-03 19:47:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 18:57:49 +0200 |
| commit | 5383050ccdaca3f1b97e06bb782e5704231e9cdb (patch) | |
| tree | 87f478e16c37354e9d1af4ef1e1889a8368f0ac0 /INSTALL.md | |
| parent | 16b2734e050d4c28d5da1a509cd2387cb8cebe6b (diff) | |
Add advisories on OCaml setup to INSTALL.md.
Closes #12232.
Diffstat (limited to 'INSTALL.md')
| -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 ...`. |