From 3b1edf7cf689a54d03226072dd3b359026588e26 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 18 Oct 2019 12:03:23 +0200 Subject: Add the IEEE-754 arch requirement in INSTALL Co-authored-by: Erik Martin-Dorel --- INSTALL | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index e30706e005..d9efd55b95 100644 --- a/INSTALL +++ b/INSTALL @@ -21,9 +21,19 @@ WHAT DO YOU NEED ? - a C compiler + - an IEEE-754 compliant architecture with rounding to nearest + ties to even as default rounding mode (most architectures + should work nowadays) + - for CoqIDE, the lablgtk development files (version >= 3.0.0), and the GTK 3.x libraries including gtksourceview3. + The IEEE-754 compliance is required by primitive floating-point + numbers (Require Import Floats). Common sources of incompatibility + are checked at configure time, preventing compilation. In the, + unlikely, event an incompatibility remains undetected, using Floats + would enable to prove False on this architecture. + Note that num and lablgtk should be properly registered with findlib/ocamlfind as Coq's makefile will use it to locate the libraries during the build. -- cgit v1.2.3