Fails when `From ... Require (Im|Ex)port ...` is used

[RalfJung]

Steps to reproduce:

• Check out https://gitlab.mpi-sws.org/FP/iris-coq.git
• Go to commit 27c7dd1
• Run find-bug.py -Q . "" algebra/cmra.v evar.v

Actual behavior:

First, I will attempt to factor out all of the [Require]s algebra/cmra.v, and store the result in evar.v...
coq_makefile COQC = coqc -Q . "" algebra/agree.v algebra/auth.v algebra/base.v algebra/cmra.v algebra/cmra_big_op.v algebra/cmra_tactics.v algebra/cofe.v algebra/cofe_solver.v algebra/dra.v algebra/excl.v algebra/fin_maps.v algebra/functor.v algebra/iprod.v algebra/option.v algebra/sts.v algebra/upred.v algebra/upred_big_op.v barrier/barrier.v heap_lang/derived.v heap_lang/heap.v heap_lang/lang.v heap_lang/lifting.v heap_lang/notation.v heap_lang/substitution.v heap_lang/tactics.v heap_lang/tests.v heap_lang/wp_tactics.v prelude/base.v prelude/bsets.v prelude/co_pset.v prelude/collections.v prelude/countable.v prelude/decidable.v prelude/error.v prelude/fin_collections.v prelude/fin_map_dom.v prelude/fin_maps.v prelude/finite.v prelude/functions.v prelude/gmap.v prelude/hashset.v prelude/lexico.v prelude/list.v prelude/listset.v prelude/listset_nodup.v prelude/mapset.v prelude/natmap.v prelude/nmap.v prelude/numbers.v prelude/option.v prelude/orders.v prelude/pmap.v prelude/prelude.v prelude/pretty.v prelude/proof_irrel.v prelude/relations.v prelude/sets.v prelude/streams.v prelude/stringmap.v prelude/strings.v prelude/tactics.v prelude/vector.v prelude/zmap.v program_logic/adequacy.v program_logic/auth.v program_logic/ghost_ownership.v program_logic/hoare.v program_logic/hoare_lifting.v program_logic/invariants.v program_logic/language.v program_logic/lifting.v program_logic/model.v program_logic/namespaces.v program_logic/ownership.v program_logic/pviewshifts.v program_logic/resources.v program_logic/saved_prop.v program_logic/sts.v program_logic/tests.v program_logic/viewshifts.v program_logic/weakestpre.v program_logic/wsat.v tmpxX6a5n.v
make -k -f - algebra/cmra.glob
"/home/r/bin/coq-8.5/bin/coqdep" -c -Q "." "" "tmpxX6a5n.v" > "tmpxX6a5n.v.d" || ( RV=$?; rm -f "tmpxX6a5n.v.d"; exit ${RV} )
"/home/r/bin/coq-8.5/bin/coqdep" -c -Q "." "" "algebra/cmra.v" > "algebra/cmra.v.d" || ( RV=$?; rm -f "algebra/cmra.v.d"; exit ${RV} )
coqc  -q  -Q "." ""   algebra/cmra
File "./algebra/cmra.v", line 218, characters 19-35:
Anomaly: cvtac's exception: Logic.RefinerError(_). Please report.
/tmp/GmyVU2Ej:321: recipe for target 'algebra/cmra.glob' failed
make: *** [algebra/cmra.glob] Error 129
getting algebra/cmra.v
getting algebra/cmra.glob

Now, I will attempt to coq the file, and find the error...

Coqing the file (evar.v)...

Running command: "coqc" "-Q" "." "" "-top" "cmra" "/tmp/tmpGFgeNh.v" "-q"
The timeout has been set to: 2

This file produces the following output when Coq'ed:
File "/tmp/tmpGFgeNh.v", line 49, characters 28-40:
Error: Cannot find a physical path bound to logical path matching suffix
algebra and prefix algebra.

Does this output display the correct error? [(y)es/(n)o] n

Expected behavior: It should get the error message right. The problem is that it turned From algebra Require Export cofe. into From algebra Require Export algebra.cofe., which is wrong.

[JasonGross]

Ugh, the From ... Require ... construct is terrible. First, From ... Import ... fails. Second, bug #4585. But I've pushed a change that adds a pass to fix this, I hope.

[RalfJung]

Not sure what you mean, From ... Require Import ... works fine. Or did you mean just Import, no Require? From is an extension of Require, not of Import or Export, it seems.

But yeah, the semantics are weird. Also see https://github.com/ProofGeneral/PG/issues/55#issuecomment-185623828.

[JasonGross]

In Coq 8.4, replacing Require Import with Require was a valid transformation. This is no longer the case in 8.5, as Require can come from From ... Require ....

[JasonGross]

By the way, thanks for the report!

[RalfJung]

Thanks for the quick fix :)