[Iris-Club] Installing the sources alongside the object files
Ralf Jung
jung at mpi-sws.org
Tue Jul 11 19:39:18 CEST 2017
Hi Dan,
> Dear Iris hackers and users,
> I am using ProofGeneral with
> [company-coq](https://github.com/cpitclaudel/company-coq) which allows
> me to have a useful shortcut M-. that jumps to a definition. The only
> issue with that: in order to jump to a definition in a module M, the
> source file M.v should be installed alongside the .vo file.
>
> Currently, I just hacked the Makefile.coq myself to add the following line:
>
> VFILES0=$(patsubst theories/%,%,$(filter theories/%,$(VFILES)))
>
> (Curiously, the makefile generated by coq_makefile already includes the
> installation process for .v files, it's just that the variable `VFILES0`
> is undefined -- does anyone know why is that?)
Actually, my Makefile.coq contains that line:
VO=vo
VOFILES:=$(VFILES:.v=.$(VO))
VOFILES0=$(patsubst theories/%,%,$(filter theories/%,$(VOFILES)))
VFILES0=$(patsubst theories/%,%,$(filter theories/%,$(VFILES)))
GLOBFILES:=$(VFILES:.v=.glob)
And the opam-installed iris (which effectively just runs "make install")
does have the source files:
> $ ls -R /home/r/.opam/coq-8.6/lib/coq/user-contrib/iris
> /home/r/.opam/coq-8.6/lib/coq/user-contrib/iris:
> algebra base_logic heap_lang program_logic proofmode tests
>
> /home/r/.opam/coq-8.6/lib/coq/user-contrib/iris/algebra:
> agree.v auth.vo big_op.v cmra_big_op.vo cofe_solver.v coPset.vo deprecated.v dra.vo frac_auth.v frac.vo gset.v iprod.vo local_updates.v monoid.vo sts.v updates.vo
> agree.vo base.v big_op.vo cmra.v cofe_solver.vo csum.v deprecated.vo excl.v frac_auth.vo gmap.v gset.vo list.v local_updates.vo ofe.v sts.vo vector.v
> auth.v base.vo cmra_big_op.v cmra.vo coPset.v csum.vo dra.v excl.vo frac.v gmap.vo iprod.v list.vo monoid.v ofe.vo updates.v vector.vo
I actually remember spending some time a while ago to make this work
(for different reasons that yours). I also remember the missing
VFILES0, but now that seems to be fixed...?
Actually, I noticed I am not using Coq 8.6, but "8.6.dev", which is to
say I am using the development version of the 8.6 branch from some point
in time some months ago. If you are using opam, could you try that and
see if it helps?
Kind regards,
Ralf
More information about the Iris-Club
mailing list