search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

help understanding sertop error #71

Open affeldt-aist opened 2 years ago

affeldt-aist commented 2 years ago

The following file test.v:

From mathcomp Require Import all_ssreflect.
From HB Require Import structures.

compiled with the following command: alectryon --frontend coq+rst --backend webpage test.v

fails with the following error message:

[sertop] Critical Dynlink error The module `Result' is already loaded (either by the main program or a previously-dynlinked library)
test.v:1: (ERROR/3) Coq raised an exception:
  > Anomaly "Uncaught exception Not_found."
  > Please report at http://coq.inria.fr/bugs/.
The offending chunk is delimited by >>>…<<< below:
  > From mathcomp Require Import all_ssreflect.>>>From HB Require Import structures.<<<
Results past this point may be unreliable.
test.v:1: (WARNING/2) Orphaned message for sid b'3':
 >  Anomaly "Uncaught exception Not_found."
 >  Please report at http://coq.inria.fr/bugs/.
make: *** [Makefile:2: alectryon] Error 13

Yet, it succeeds if one removes the line about HB. (So this does not look like a failure to find the libraries.)

What could be the problem? (I am using a recently cloned alectryon, Coq 8.13.2, the last opam version of coq-serapi.)

Zimmi48 commented 2 years ago

This is a SerAPI issue, worth reporting upstream. It can be reproduced within sertop with:

(Add () "From mathcomp Require Import all_ssreflect.")
(Add () "From HB Require Import structures.")