coq lin-alg-8.10 seems to install (with coq 8.9 or 8.10?) but doesn't appear in opam list

Question

coq lin-alg-8.10 seems to install (with coq 8.9 or 8.10?) but doesn't appear in opam list

brando90 opened this issue 2 years ago · 4 comments

I installed it with the suggested command but fails to appear in opam list, full output:

(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
(iit_synthesis) brando9~/proverbot9001 $

Answer 1 · 2023-02-13T22:41:48.000Z

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.

Answer 2 · 2023-02-13T22:52:41.000Z

old lin-alg discussion: #61

Answer 3 · 2023-02-13T23:04:42.000Z

how to verify install: https://stackoverflow.com/questions/75441920/how-does-one-make-sure-that-coq-project-installed-correctly-when-it-doesnt-seem

Answer 4 · 2023-02-14T19:38:09.000Z

I think the answer you have on that stack overflow should be sufficient here