Newbie problem in CoqIDE on windows

Using Coq
1

Hi all,
I am an absolute newbie to Coq; I have just downloaded and and run the installer for windows. I plan to use the built-in GAPPA functionality in order to obtain and compare error bounds for floating-point calculations that can be formulated in several mathematically equivalent ways.
Unfortunately, the error message
“Unable to locate library Fcore.”
pops up when I try to execute the following example, the first lines of which I have compiled from the GAPPA manual:
Require Import Reals.
Require Import Fcore.
Require Import Gappa_tactic.
Open Scope R_scope.
@rnd = float< ieee_64, ne >;
xsq = xx*xx;
xsqrnd = rnd(xsq);
omxsq = 1-xsq;
omxsqrnd = rnd(1-xsqrnd);
sqrtomxsq = sqrt(omxsq);
sqrtomxsqrnd = rnd(sqrtomxsq);
errout = (sqrtomxsqrnd - sqrtomxsq);
{ xx in [0,1] -> |errout| in ? };
Importing “Reals” works, but importing “Fcore” does not.
What am I missing? I checked every box I could find in during installation.
I have already replaced “V8.9.1” by “current” in the two hardcoded path entries for refman and stdlib, resp., in the file coqiderc found in $home\AppData\Local\coq. The help now works, but “Fcore” still is not found.

All the best
Schorsch

2

Hello.

It may be the case that gappa’s manual is a bit outdated. Ping @silene.

If in your preamble, you instead write:

From Coq Require Import Reals.
From Flocq Require Import Core.
From Gappa Require Import Gappa_tactic.
Open Scope R_scope.

then you can run the examples from the “Coq and Gappa” chapter of the manual.

Tested with Coq 8.9.1, Flocq 3.1.0, gappalib 1.4.1 and gappa 1.3.5.

3

Thank you very much for your detailed hints, Vincent!
From browsing the Coq library I meanwhile had concluded that the second and third modules mentioned in the script do not exist (anymore).
I will soon try out your preamble and the examples you pointed me to.
Thx
Schorsch