ci: also test trocq

Author: gares

.github/workflows/users.yml

@@ -30,16 +30,19 @@ jobs:
           env:
             OPAMWITHTEST: false
 
-        - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#master
-        - run: opam pin --ignore-constraints-on elpi add coq-elpi  https://github.com/LPCIC/coq-elpi.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-stdlib https://github.com/rocq-prover/stdlib.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-boot https://github.com/math-comp/math-comp.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-order https://github.com/math-comp/math-comp.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-algebra https://github.com/math-comp/math-comp.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-solvable https://github.com/math-comp/math-comp.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-field https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-elpi              https://github.com/LPCIC/coq-elpi.git#master
+        - run: opam pin --ignore-constraints-on elpi            add coq-elpi               https://github.com/LPCIC/coq-elpi.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-stdlib            https://github.com/rocq-prover/stdlib.git#master
+        - run: opam pin --ignore-constraints-on elpi            add coq-stdlib             https://github.com/rocq-prover/stdlib.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
+        - run: opam pin --ignore-constraints-on elpi,coq-stdlib add coq-trocq-std          https://github.com/rocq-community/trocq.git#fix-opam-install
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-boot     https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-order    https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-algebra  https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi,coq-stdlib add coq-trocq-std-examples https://github.com/rocq-community/trocq.git#fix-opam-install
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-solvable https://github.com/math-comp/math-comp.git#master
+        - run: opam pin --ignore-constraints-on elpi            add rocq-mathcomp-field    https://github.com/math-comp/math-comp.git#master
 
     # test-users-br:
     #   name: "test users: bluerock.io"