 24 Jul, 2019 1 commit


Pierre Roux authored

 19 Jul, 2019 1 commit


Maxime Lesourd authored
This is a port (+additions) of the definitions and semantics for arrival curves (model/arrival/curves.v). As a prerequisite, this includes definitions about activations of a task (model/task_arrivals.v). Two additional definitions which were not found in the original library but will be useful to us in the future: * in schedule.v : completes_at * in task_arrivals.v : arrivals_come_from_taskset

 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/coqcommunity/dockercoq/wiki/CIsetup Using the following CI template as a starting point: https://gitlab.com/erikmd/dockercoqgitlabcidemo1/blob/master/.gitlabci.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 1 commit


Björn Brandenburg authored
