help understanding sertop error

[affeldt-aist]

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]

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.")