英文:
How does one make sure that coq project installed correctly when it doesn't seem to appear on opam list?
问题
I installed lin-alg-8.10 using the instructions provided in proverbot's repo for Coq 8.10, and here is the full output of the commands:
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/lin-alg && make "$@" && make install)
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make -f Makefile.coq all
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[2]: Nothing to be done for 'real-all'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make -f Makefile.coq install
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
INSTALL first_page.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg/
INSTALL support/equal_syntax.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/more_syntax.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/vecspaces_verybasic.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
...
(Installation of various files continues)
To confirm whether lin-alg-8.10 was installed correctly under Coq version 8.10, you can check if the installation directory and files exist in your Opam environment.
英文:
I tried installing lin-alg-8.10 using the instructions I was told from proverbot's repo using coq 8.10:
# - Create the 8.10 switch
opam switch
opam switch create coq-8.10 4.07.1
eval $(opam env --switch=coq-8.10 --set-switch)
opam pin add -y coq 8.10.2
git submodule add -f --name coq-projects/lin-alg-8.10 git@github.com:HazardousPeach/lin-alg-8.10.git coq-projects/lin-alg
git submodule update --init coq-projects/lin-alg
#
(cd coq-projects/lin-alg && make "$@" && make install)
after a long set of output of the commands it seems it installed -- due to the lack of errors -- but grepping opam list gives literally no output.
How do I confirm I did install lin-alg-8.10 correctly under the stuggested coq version (I assume 8.9)?
Full output of commands:
(iit_synthesis) brando9~/proverbot9001 $ (cd coq-projects/lin-alg && make "$@" && make install)
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make -f Makefile.coq all
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[2]: Nothing to be done for 'real-all'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make -f Makefile.coq install
make[1]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
INSTALL first_page.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg/
INSTALL support/equal_syntax.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/more_syntax.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/vecspaces_verybasic.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/finite.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_Fn.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/Map2.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_functionspace.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrices.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/vecspace_Mmn.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL LinAlg/alt_build_vecsp.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/infinite_sequences.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/algebra_omissions.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/arb_intersections.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/subspaces.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/antisymmetric_matrices.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/symmetric_matrices.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/up_lo_triang_mat.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/seq_set.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_seq.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/empty.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/conshdtl.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/const.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/pointwise.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/modify_seq.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/mult_by_scalars.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/Map_embed.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/subseqs.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums2.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_seq_lengths.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distribution_lemmas.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_between_subsets.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/lin_combinations.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/spans.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/algebraic_span_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_comb_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/direct_sum.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dependence.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dep_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/random_facts.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/finite_subsets.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/has_n_elements.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/counting_elements.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/bases.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_from_generating_sets.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_theorem.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_corollaries.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_finite_dim.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/maxlinindepsubsets.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_dim.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_bases.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Lin_trafos.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/trivial_spaces.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrix_multiplication.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL extras/ring_module.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Inter_intersection.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/finite_misc.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/restrict.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Matrix_related_defs.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/before_after.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/matrix_algebra.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Equality_structures.vo /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL first_page.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg/
INSTALL support/equal_syntax.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/more_syntax.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/vecspaces_verybasic.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/finite.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_Fn.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/Map2.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_functionspace.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrices.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/vecspace_Mmn.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL LinAlg/alt_build_vecsp.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/infinite_sequences.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/algebra_omissions.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/arb_intersections.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/subspaces.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/antisymmetric_matrices.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/symmetric_matrices.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/up_lo_triang_mat.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/seq_set.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_seq.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/empty.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/conshdtl.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/const.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/pointwise.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/modify_seq.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/mult_by_scalars.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/Map_embed.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/subseqs.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums2.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_seq_lengths.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distribution_lemmas.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_between_subsets.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/lin_combinations.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/spans.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/algebraic_span_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_comb_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/direct_sum.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dependence.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dep_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/random_facts.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/finite_subsets.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/has_n_elements.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/counting_elements.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/bases.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_from_generating_sets.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_theorem.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_corollaries.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_finite_dim.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/maxlinindepsubsets.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_dim.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_bases.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Lin_trafos.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/trivial_spaces.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrix_multiplication.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL extras/ring_module.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Inter_intersection.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/finite_misc.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/restrict.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Matrix_related_defs.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/before_after.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/matrix_algebra.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Equality_structures.v /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL first_page.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg/
INSTALL support/equal_syntax.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/more_syntax.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/vecspaces_verybasic.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/finite.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_Fn.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/Map2.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL examples/vecspace_functionspace.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrices.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/vecspace_Mmn.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL LinAlg/alt_build_vecsp.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/infinite_sequences.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/algebra_omissions.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/arb_intersections.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/subspaces.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/antisymmetric_matrices.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/symmetric_matrices.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/up_lo_triang_mat.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL support/seq_set.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_seq.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/empty.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/conshdtl.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/const.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/pointwise.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/modify_seq.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/mult_by_scalars.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/Map_embed.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/subseqs.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/sums2.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_seq_lengths.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/concat_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_equality_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distribution_lemmas.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/seq_set_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/omit_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/distinct_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/cast_between_subsets.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/lin_combinations.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/spans.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/algebraic_span_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_comb_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/direct_sum.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dependence.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/lin_dep_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL support/random_facts.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/finite_subsets.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/has_n_elements.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL support/counting_elements.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//support
INSTALL LinAlg/bases.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_from_generating_sets.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_theorem.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/replacement_corollaries.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/bases_finite_dim.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/maxlinindepsubsets.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_dim.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/subspace_bases.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL LinAlg/Lin_trafos.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//LinAlg
INSTALL examples/trivial_spaces.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL examples/Matrix_multiplication.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//examples
INSTALL extras/ring_module.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Inter_intersection.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/finite_misc.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/restrict.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Matrix_related_defs.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/before_after.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/matrix_algebra.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
INSTALL extras/Equality_structures.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
make[2]: Entering directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[2]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
make[1]: Leaving directory '/afs/cs.stanford.edu/u/brando9/proverbot9001/coq-projects/lin-alg'
(iit_synthesis) brando9~/proverbot9001 $ opam list | grep lin-alg
Was it installed with coq 8.9 or 8.10?
it is also very confusing which coq version is using given the final output of the opam switch command:
(iit_synthesis) brando9~/proverbot9001 $ opam switch
# switch compiler description
→ coq-8.10 ocaml-base-compiler.4.07.1 coq-8.10
coq-8.15 ocaml-base-compiler.4.07.1 coq-8.15
coq-8.9 ocaml-base-compiler.4.07.1 coq-8.9
default ocaml.5.0.0 default
[NOTE] Current switch is set locally through the OPAMSWITCH variable.
The current global system switch is coq-8.9.
related links:
-
similar issue from git repo: https://github.com/UCSD-PL/proverbot9001/issues/81
-
old failed installation using
(cd coq-projects/lin-alg && make "$@" && make install)https://github.com/UCSD-PL/proverbot9001/issues/61 -
lin-alg-8.10 doesn't seem to be the official lin-alg repo so here is the link to the repo I am using: https://github.com/HazardousPeach/lin-alg-8.10
-
discussion that coq 8.9 might be the right coq version: https://github.com/coq-contribs/lin-alg/issues/5
答案1
得分: 1
but grepping
opam listgives literally no output.
但是在opam list中使用grepping实际上没有任何输出。
This is normal. make install just copies files around but does not update opam's own package registry (because make install is agnostic to opam). Hence packages installed that way won't appear in opam list.
这是正常的。make install 只是将文件复制到其他地方，但不会更新 opam 的包注册表（因为 make install 与 opam 无关）。因此，通过这种方式安装的包不会出现在 opam list 中。
You can install local versions of packages using something like opam pin add coq-lin-alg /path/to/lin-alg-8.10 (but this can be brittle if a released package has changed its build script in the meantime).
你可以使用类似 opam pin add coq-lin-alg /path/to/lin-alg-8.10 的方法安装本地版本的包（但如果已发布的包在此期间更改了其构建脚本，这可能会很脆弱）。
How do I confirm I did install lin-alg-8.10 correctly under the suggested coq version (I assume 8.9)?
如何确认我在建议的 Coq 版本下（我假设是 8.9）正确安装了 lin-alg-8.10？
Look at the paths in the install output:
查看安装输出中的路径：
INSTALL extras/Equality_structures.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
The name of the switch can be seen as a directory: .../.opam/coq-8.10/....
开关的名称可以看作是一个目录：.../.opam/coq-8.10/...。
The next step is to open a new Coq file and try to Require Import a module from the newly installed library.
下一步是打开一个新的 Coq 文件并尝试从新安装的库中使用 Require Import 导入一个模块。
it is also very confusing which coq version is using given the final output of the
opam switchcommand
考虑到opam switch命令的最终输出，使用哪个 Coq 版本也很令人困惑。
The answer to "What coq version is CURRENTLY being used" is in the first part of the output (where the arrow points to), ignoring the warning. The warning tells you that it will no longer be the case once the environment variable OPAMSWITCH is unset, which will probably be when you open a new terminal (unless a start-up script sets it again, but you probably shouldn't use --set-switch to begin with, see below).
答案是“当前使用的 Coq 版本”在输出的第一部分中（箭头指向的部分），忽略警告。警告告诉您，一旦取消设置环境变量 OPAMSWITCH，这将不再是情况，这可能是在您打开一个新终端时（除非启动脚本再次设置它，但您可能不应该一开始使用 --set-switch，请参见下文）。
You would have a less confusing output if you switched like this:
如果您像这样切换，输出将会更清晰：
opam switch coq-8.10
eval $(opam env)
# Check: no warnings
opam switch
instead of
而不是
eval $(opam env --switch=coq-8.10 --set-switch)
# Check: warning (if the global switch isn't 8.10 already)
opam switch
# ...
[NOTE] Current switch is set locally through the OPAMSWITCH variable.
The current global system switch is coq-8.9.
英文:
> but grepping opam list gives literally no output.
This is normal. make install just copies files around but does not update opam's own package registry (because make install is agnostic to opam). Hence packages installed that way won't appear in opam list.
You can install local versions of packages using something like opam pin add coq-lin-alg /path/to/lin-alg-8.10 (but this can be brittle if a released package has changed its build script in the meantime).
> How do I confirm I did install lin-alg-8.10 correctly under the stuggested coq version (I assume 8.9)?
Look at the paths in the install output:
INSTALL extras/Equality_structures.glob /lfs/ampere1/0/brando9/.opam/coq-8.10/lib/coq//user-contrib/LinAlg//extras
The name of the switch can be seen as a directory: .../.opam/coq-8.10/....
The next step is to open a new Coq file and try to Require Import a module from the newly installed library.
> it is also very confusing which coq version is using given the final output of the opam switch command
The answer to "What coq version is CURRENTLY being used" is in the first part of the output (where the arrow points to), ignoring the warning. The warning tells you that it will no longer be the case once the environment variable OPAMSWITCH is unset, which will probably be when you open a new terminal (unless a start-up script sets it again, but you probably shouldn't use --set-switch to begin with, see below).
You would have a less confusing output if you switched like this:
# Global switch (persists across shell sessions)
opam switch coq-8.10
eval $(opam env)
# Check: no warnings
opam switch
instead of
# Local switch (via environment variables; only for the current session)
eval $(opam env --switch=coq-8.10 --set-switch)
# Check: warning (if the global switch isn't 8.10 already)
opam switch
# ...
[NOTE] Current switch is set locally through the OPAMSWITCH variable.
The current global system switch is coq-8.9.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论