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 [email protected]: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
This is normal.
make installjust copies files around but does not updateopam's own package registry (becausemake installis agnostic toopam). Hence packages installed that way won't appear inopam 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).Look at the paths in the install output:
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 Importa module from the newly installed library.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
OPAMSWITCHis 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-switchto begin with, see below).You would have a less confusing output if you switched like this:
instead of