- 05 Jul, 2019 1 commit
-
-
Xiaojie Guo authored
-
- 02 Jul, 2019 2 commits
-
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
- 27 Jun, 2019 1 commit
-
-
Maxime Lesourd authored
-
- 26 Jun, 2019 1 commit
-
-
Maxime Lesourd authored
simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model
-
- 25 Jun, 2019 1 commit
-
-
Björn Brandenburg authored
- Consistently use JobType rather than eqType directly. - Fix the comments style.
-
- 12 Jun, 2019 3 commits
-
-
Björn Brandenburg authored
Coqdoc produces really nice output - let's automate this.
-
Björn Brandenburg authored
There's no need to run this for every compiler version; we only care about the "main" version.
-
Björn Brandenburg authored
This avoids having to compile ssreflect from scratch each time we want to compile Prosa. Thanks to Pierre Roux (Pierre.Roux@onera.fr) for pointing out the mathcomp Docker images!
-
- 05 Jun, 2019 17 commits
-
-
Sergey Bozhko authored
-
Björn Brandenburg authored
From the mathcomp 1.9.0 release notes: > removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to > improve robustness of by ...; scripts may need to invoke addn0, > addnS, muln0 or mulnS explicitly where these hints were used > accidentally. => This patch makes these required fixes in Prosa. While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Maxime Lesourd authored
-
Björn Brandenburg authored
Using the official Coq Docker images kindly provided by the Coq community: https://github.com/coq-community/docker-coq/wiki/CI-setup Using the following CI template as a starting point: https://gitlab.com/erikmd/docker-coq-gitlab-ci-demo-1/blob/master/.gitlab-ci.yml
-
- 26 May, 2019 1 commit
-
-
Sergey Bozhko authored
-
- 19 May, 2019 1 commit
-
-
Sergey Bozhko authored
-
- 16 May, 2019 10 commits
-
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
Björn Brandenburg authored
...and introduce a bunch of helper lemmas to get there.
-
Björn Brandenburg authored
-
Björn Brandenburg authored
Let's not clutter up the spec with facts files all over the place. Instead, let's collect the facts files in a separate folder / hierarchy.
-
Björn Brandenburg authored
-
Björn Brandenburg authored
- port completed_implies_scheduled_before - port lemmas on service prior to arrival - port scheduled_implies_pending and greatly simplify the proof while at it - port and simplify job_pending_at_arrival - port cumulative_service_implies_scheduled and simplify proof of positive_service_implies_scheduled_before - port service_is_a_step_function
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-
- 13 May, 2019 2 commits
-
-
Björn Brandenburg authored
-
Björn Brandenburg authored
-