From 8ca362b2bb2aeb1bd992c064eb1e23cf44dffdf6 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Tue, 22 Feb 2022 17:09:00 +0100
Subject: [PATCH] Clean table of content
---
doc/tutorial.v | 116 +++----------------------------------------------
1 file changed, 5 insertions(+), 111 deletions(-)
diff --git a/doc/tutorial.v b/doc/tutorial.v
index 5586fadfc..5b4885e07 100644
--- a/doc/tutorial.v
+++ b/doc/tutorial.v
@@ -604,6 +604,8 @@ Model
=====
TODO describe model
+
+test maths :math:`\sum_{i=1}^n i^2`
|*)
(*|
@@ -665,121 +667,13 @@ if Coq can compile the `Qed` it managed to check the proof and the new lemma
is now available for use in future proofs.
|*)
-(*|
-Job Properties
---------------
-
-TODO: retrieve/update material from Borislav's document on fixed priority policy and EDF
-|*)
-
-(*|
-Platform
---------
-
-TODO: retrieve/update material from Borislav's document about schedulers
-|*)
-
-(*|
-Groups of Jobs
---------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Job Schedulability
-------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Busy Interval
--------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Workload Abstraction and Workload Bounds
-----------------------------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Tasks with respect to schedules, priorities, workload, service and schedulers
------------------------------------------------------------------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Response Time Bounds
---------------------
-
-TODO: retrieve/update material from Borislav's document
-(and maybe move here the definition that was already given much earlier)
-|*)
-
-(*|
-Tasks Schedulability
---------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Task Arrival Bounds
--------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Workload bounds
----------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Task Response-Time Bound
-------------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
-(*|
-Task Response-Time Bound Computation
-------------------------------------
-
-TODO: retrieve/update material from Borislav's document
-
-test maths :math:`\sum_{i=1}^n i^2`
-|*)
-
-(*|
-Task Response-Time Bound Computation
-------------------------------------
-
-TODO: retrieve/update material from Borislav's document
-
-should we say a few words about CERTA ?
-|*)
-
-(*|
-Prosa Parts not Covered in this Document
-----------------------------------------
-
-TODO: retrieve/update material from Borislav's document
-|*)
-
(*|
Contributing
============
-TODO (link to the end of the README)
+TODO short conclusion, you should now be able to read doc by yourself
+
+TODO Prosa open source, contributions welcome (link to the end of the README)
|*)
(*|
--
GitLab