results/fixed_priority/rta/bounded_pi.v

@@ -199,7 +199,7 @@ Section AbstractRTAforFPwithArrivalCurves.
        Recall that in module abstract_seq_RTA hypothesis task_interference_is_bounded_by expects 
        to receive a function that maps some task t, the relative arrival time of a job j of task t, 
        and the length of the interval to the maximum amount of interference (for more details see 
-       files limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
+       the modules [limited.abstract_RTA.definitions] and [limited.abstract_RTA.abstract_seq_rta]).
 
        However, in this module we analyze only one task -- [tsk], therefore it is “hard-coded” 
        inside the interference bound function [IBF_other]. Moreover, in case of a model with fixed 
@@ -253,7 +253,7 @@ Section AbstractRTAforFPwithArrivalCurves.
 
       (** Given any job j of task [tsk] that arrives exactly A units after the beginning of 
          the busy interval, the bound of the total interference incurred by j within an 
-         interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other Δ]. *)
+         interval of length [Δ] is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other Δ]. *)
       Let total_interference_bound tsk A Δ :=
         task_rbf (A + ε) - task_cost tsk + IBF_other Δ.
 

scripts/extract-comments.py

@@ -6,6 +6,7 @@ import os
 import re
 
 INLINE_CODE_RE = re.compile(r'\[[^]]*?\]')
+VERBATIM_RE = re.compile(r'<<.*?>>')
 
 def comment_ranges(src):
     "Identify comments in Coq .v files."
@@ -41,8 +42,10 @@ def process(opts, fname):
     out = sys.stdout
     for (a, b) in comment_ranges(src):
         txt = src[a:b]
-        print(INLINE_CODE_RE.sub('', txt))
-#     out.close()
+        txt = txt.replace('\n', ' ')
+        txt = VERBATIM_RE.sub('', txt)
+        txt = INLINE_CODE_RE.sub('', txt)
+        print(txt)
 
 def parse_args():
     parser = argparse.ArgumentParser(

scripts/flag-typos-in-comments.sh

@@ -10,8 +10,7 @@ do
 
 	#Here, sed is used to remove verbatim text (enclosed in <<>>)
 	for WORD in $(scripts/extract-comments.py "$SRC" \
-		| sed 's/<<.*>>//g' \
-		| aspell --add-extra-dicts=$KNOWN_EXCEPTIONS -l en  list \
+		| hunspell -p $KNOWN_EXCEPTIONS -l -d en_US \
 		| sort \
 		| uniq)
 	do

scripts/wordlist.pws

-personal_ws-1.1 en 0
-Prosa
+ad hoc
+aRTA/S
+BCET/M
+bursty
 Coq
-ssreflect's
-ssreflect
-typeclass
-iff
-schedulability
-schedulable
-computable
-boolean
-disjunction
-invariant
-invariants
-instantiation
-instantiations
-uniprocessor
-uniprocessors
-jitter
-monotonicity
-antisymmetric
-optimality
-namespace
-nonpreemptive
-preemptive
-preemptable
-preemptions
+DM
+ECRTS
 EDF
+et al
+extremum
+fixpoint/M
+formedness
 FP
-DM
-POSIX
-JLFP
+Gonthier
+hyperperiod/M
+IBF/M
+iff
+instantiation/MS
 JLDP
-TDMA
-aRTA
-RTA
-IBF
-RBF
-RBFs
-WCET
-WCETs
-BCET
-BCETs
+JLFP
 Layland
+Leontyev
 Liu
-sequentiality
-equalities
-extremum
-supremum
-runtime
-bursty
-TODO
+Maida
 mathcomp
-hyperperiod
-hyperperiods
-pointwise
-notational
 multiset
-superset
+namespace
+nonpreemptive
+POET/MS
+pointwise
+POSIX
+preemptable
+preemption/M
+preemptive
+Prosa/M
+RBF/M
+rewritable
+RTA/M
 RTCT
-superadditivity
-superadditive
-subadditivity
-subadditive
-subinterval
-subsequences
-summand
-summands
-afore
-ad
-hoc
-mailinglist
-Gonthier
+schedulability
+schedulable
+sequentiality
 setoid
-Leontyev
-et
-al
-discoverable
-formedness
-unary
-rewritable
-ECRTS
-Maida
-POET's
-coercions
-unsatisfiable
-fixpoint
-fixpoints
-RTA's
-parametrized
+ssreflect/M
+subadditive
+subadditivity
+summand/M
+superadditive
+superadditivity
+superset
+supremum
+TDMA
+TODO
+typeclass
+uniprocessor/M
+WCET/M
\ No newline at end of file

util/list.v

@@ -157,7 +157,7 @@ Section Max0.
   Proof. by intros; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC. Qed.
 
   (** We prove that [max0] of a sequence [xs] 
-      is equal to [max0] of sequence [xs] without 0s. *)
+      is equal to [max0] of [xs] without any zeros. *)
   Lemma max0_rem0 :
     forall xs, 
       max0 ([seq x <- xs | 0 < x]) = max0 xs.

util/setoid.v

 (** Setoid Rewriting with boolean inequalities of ssreflect. Solution
-    suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016) *)
+    suggested by Georges Gonthier (ssreflect mailing list @ 18.12.2016) *)
 
 From Coq Require Import Basics Setoid Morphisms.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

util/sum.v

@@ -214,7 +214,7 @@ End SumsOverSequences.
 (** In this section, we prove a variety of properties of sums performed over ranges. *)
 Section SumsOverRanges.
 
-  (** First, we prove that the sum of Δ ones is equal to Δ     . *)
+  (** First, we prove that the sum of [Δ] ones is equal to [Δ]. *)
   Lemma sum_of_ones:
     forall t Δ,
       \sum_(t <= x < t + Δ) 1 = Δ.

util/tactics.v

@@ -72,12 +72,12 @@ Ltac feed H :=
   end.
 
 (* Generalization of feed for multiple hypotheses.
-   feed_n is useful for accessing conclusions of long implications.
+   [feed_n[ is useful for accessing conclusions of long implications.
 
-   Usage: feed_n 3 H.
-     H: P1 -> P2 -> P3 -> Q.
+   Usage: <<feed_n 3 H.>>
+     <<H: P1 -> P2 -> P3 -> Q.>>
 
-   We'll be asked to prove P1, P2 and P3, so that Q can be inferred. *)
+   We'll be asked to prove [P1], [P2] and [P3], so that Q can be inferred. *)
 Ltac feed_n n H := match constr:(n) with
   | O => idtac
   | (S ?m) => feed H ; [| feed_n m H]