coq-flocq does not install sources

[vzaliva]

The install target of coq-flocq does not install sources. Most opam-installed coq libraries install sources (.v files) along with compiled versions (.vo). This is convenient as it allows to examine definitions from IDE (ProofGeneral) during development.

[Zimmi48]

cc @silene

[vzaliva]

I've created a patch to solve this issue. Unfortunately, Flocq is hosted at gitlab.inria.fr which does not allow pull requests from external contributors :(

--- flocq-3.0.0/Remakefile.in	2018-04-04 05:28:08.000000000 -0700
+++ flocq/Remakefile.in	2018-08-29 11:32:06.877169752 -0700
@@ -127,6 +127,7 @@
 	mkdir -p @libdir@
 	for d in Core Calc Prop IEEE754 Pff; do mkdir -p @libdir@/$d; done
 	for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
+	for f in $(FILES); do cp src/$f @libdir@/${f}; done
 	( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
 
 EXTRA_DIST = \

[Zimmi48]

You can still create an account, and open an issue on the Flocq repository with your patch. Maybe it has better chances of grabbing @silene's attention.

[vzaliva]

https://gitlab.inria.fr/flocq/flocq/issues/3

[vzaliva]

My patch was applied at gitlab.inria.fr 3 months ago. However, this version has not made its way into opam repository so we could not benefit from it.

[Zimmi48]

I think @silene is prioritizing releasing the next version of Coq over releasing a new version of Flocq for now.

[clarus]

@vzaliva It seems to me that the latest version of coq-flocq does install the .v. Thus your patch got published. Do you confirm?

[vzaliva]

Yes, the sources are correctly installed in coq-flocq-3.2.0