coq/test-suite/misc/universes, branch master The formal proof system Dune: fix build_all_stdlib rule 2019-07-21T15:05:48+00:00 Gaëtan Gilbert 2019-07-21T15:05:07+00:00 f1206ec5d6c6d7f557ec6802e64b41d82fc806f8 The issue could be reproduced by doing "dune build test-suite/misc/universes/all_stdlib.v" (from a clean build) which would error 127 with no message. - only redirect stdout so that in the future we will see error messages - put the script as a dependency (I guess it sometime succeeded when copying the deps for the test suite happened before running it) 
The issue could be reproduced by doing "dune build
test-suite/misc/universes/all_stdlib.v" (from a clean build) which
would error 127 with no message.

- only redirect stdout so that in the future we will see error
  messages

- put the script as a dependency (I guess it sometime succeeded when
  copying the deps for the test suite happened before running it)
[dune] Fix Dune build in Windows. 2019-02-04T17:16:39+00:00 Emilio Jesus Gallego Arias 2019-02-04T17:16:39+00:00 0439543db9f3be84d59cfdc1dcad34bd114036e3 In order for Dune to work in Windows we need to tweak some script calls, they need a POSIX shell and the `(run ...)` / `(system ...)` actions use `cmd.exe` on Windows. Hopefully, we will rely less on `bash` when Dune can understand Coq libraries. This affects shell scripts in `kernel/**.sh` for example. It is interesting to see how faster the Coq Windows build is with Dune + Windows. There are some problems with PATHs that prevent the test suite from working, these will be fixed in a future PR. 
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.

Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.

It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.

There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
[dune] [test-suite] Support for running the test suite with Dune. 2018-10-11T12:32:33+00:00 Emilio Jesus Gallego Arias 2018-09-26T20:49:20+00:00 9e39d88ffb5829a9e2c82fbf54c0765a819b3e5e 






Add a test for sorting all universes of stdlib
2011-01-25T07:02:13+00:00

glondu

2011-01-25T07:02:13+00:00

8966d6291e76dba17bedd5f04402d4cd5f4e9da7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7