Configuration CoqIDE sous Linux

Question

J'ai une nouvelle installation de Coq 8.6 sous Ubuntu 17.04. Lorsque j'essaie de compiler mon projet en utilisant make, cela fonctionne bien jusqu'à ce que j'obtienne le premier message d'erreur. Ensuite, je tente d'utiliser CoqIDE pour localiser et corriger l'erreur, mais je reçois de nouveaux messages d'erreur, tels que:

« Le foo.vo fichier contient la bibliothèque Top.foo et non bibliothèque foo »

Je pense est que quelque chose ne va pas avec la configuration de CoqIDE, mais je ne sais pas ce que cela pourrait être. Des indices? Merci d'avance, Marcus.

Answer 1

Je suppose que vous êtes maintenant debout dans le répertoire avec le fichier foo.vo

Pour mapper les fichiers du répertoire . en cours dans l'espace de noms Top vous donnez l'argument

-Q . Top 

Voici un " compléter "exemple.

mkdir test; cd test 
echo 'Definition a:=1.' > foo.v 

coqc -Q . Top foo.v # this puts the foo module into Top as Top.foo. 

coqtop -Q . Top 

Coq < Require Import Top.foo. Print a. 

a = 1 
    : nat 

mais en utilisant coqtop sans mapper le .vo à l'espace dans lequel il a été compilé échoue:

coqtop 

Coq < Require foo. 

> Require foo. 
> ^^^^^^^^^^^^ 
Error: The file /.../test/foo.vo contains library Top.foo 
and not library foo