Doesn't build with Coq 8.6

[wilbowma]

COQC Autosubst_MMap.v
File "./Autosubst_MMap.v", line 26, characters 0-37:
Error: Some argument names are duplicated: H

Full log:

make -C theories
make[1]: Entering directory 'src/autosubst-1.6/theories'
coq_makefile -R . Autosubst Autosubst_Derive.v Autosubst.v Autosubst_MMapInstances.v Autosubst_Classes.v Autosubst_Basics.v Autosubst_Lemmas.v Autosubst_MMap.v Autosubst_Tactics.v -o Makefile.coq
make -f Makefile.coq all
make[2]: Entering directory 'src/autosubst-1.6/theories'
COQDEP Autosubst_Lemmas.v
COQDEP Autosubst_Tactics.v
COQDEP Autosubst_MMap.v
COQDEP Autosubst_Classes.v
COQDEP Autosubst_Basics.v
COQDEP Autosubst_MMapInstances.v
COQDEP Autosubst.v
COQDEP Autosubst_Derive.v
COQC Autosubst_Basics.v
File "./Autosubst_Basics.v", line 76, characters 27-40:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 78, characters 29-42:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 119, characters 11-27:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
fun (f : var -> var) (sigma : var -> list var) =>
nil .: nil .: f >>> f >>> nil .: nil .: f >>> f >>> nil .: nil .: sigma
     : (var -> var) -> (var -> list var) -> var -> list var
File "./Autosubst_Basics.v", line 272, characters 10-26:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 276, characters 10-43:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 290, characters 6-22:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
File "./Autosubst_Basics.v", line 294, characters 6-39:
Warning: appcontext is deprecated and will be removed in a future version
[deprecated-appcontext,deprecated]
COQC Autosubst_MMap.v
File "./Autosubst_MMap.v", line 26, characters 0-37:
Error: Some argument names are duplicated: H
make[2]: *** [Makefile.coq:272: Autosubst_MMap.vo] Error 1
make[2]: Leaving directory 'src/autosubst-1.6/theories'
make[1]: *** [Makefile:8: all] Error 2
make[1]: Leaving directory 'src/autosubst-1.6/theories'
make: *** [Makefile:21: lib] Error 2

[landaro]

Thanks for bringing this to our attention. We are currently working on a version that will work with Coq 8.6.

kind regards, Jonas

[landaro]

Update: There is now a coq86-devel branch. It is still work in progress, but so far,

make make examples-plain

should work, and the resulting package should work with most of the existing client code. So far I was only able to test the update on a single larger development, but there the only necessary adjustments where due to the changes in automatic name generation of Coq 8.6 and nothing particular to autosubst.

I am not familiar with Ssreflect, so the ssr examples are not yet ported. We also would like to perform some more testing, before merging the fix back into master.

Anybody who is willing to experiment with the fix is welcome to switch to the coq86-devel branch for now.

Best, Jonas

[co-dan]

I managed to compile my small codebase with the coq86-devel and it appears to be working fine.

[sfs]

I just pushed a fix for the remaining ssreflect examples and can confirm that it now builds with Coq trunk without issues.

@landaro can you test this on Coq 8.6 and then merge into master? Thanks.

[rnrand]

Looks like the 8.6 dev version was never merged.

If you can't merge the fix into master, could you add a pointer to the 8.6 version to the Readme? That way potential users know which version to install.

[takanuva]

Same issue here.

[Blaisorblade]

FWIW, coq86-devel also works in Coq 8.8 (after opam install coq-mathcomp-ssreflect, version 1.7).

[Blaisorblade]

@rnrand Created a PR for the README as you suggested.

[RalfJung]

Master now works with Coq 8.9 and later. Coq 8.6 is not supported any more, so I will close this issue.