Merge remote-tracking branch 'origin/master' into gen_proofmode

benchmark/.gitignore

 __pycache__
-build-times.log*
+build-times*
 gitlab-extract

benchmark/export.py

@@ -3,8 +3,6 @@ import argparse, sys, pprint, itertools, subprocess
 import requests
 import parse_log
 
-markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
-
 # read command-line arguments
 parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana')
 parser.add_argument("-f", "--file",
@@ -19,6 +17,9 @@ parser.add_argument("-p", "--project",
 parser.add_argument("-b", "--branch",
                     dest="branch", required=True,
                     help="Branch name sent to the server.")
+parser.add_argument("--config",
+                    dest="config", required=True,
+                    help="The config string.")
 parser.add_argument("-s", "--server",
                     dest="server", required=True,
                     help="The server (URL) to send the data to.")
@@ -39,10 +40,11 @@ if args.commits:
 results = list(results)
 
 for datapoint in results:
-    times = ''.join(datapoint.times)
+    times = '\n'.join(datapoint.times)
     commit = datapoint.commit
+    print("Sending {}...".format(commit), end='')
     date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8')
-    headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Date': date}
-    r = requests.post(args.server, data=times, headers=headers, auth=(args.user, args.password))
+    headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
+    r = requests.post(args.server+"/build_times_8.6", data=times, headers=headers, auth=(args.user, args.password))
+    print(" {}".format(r.text.strip()))
     r.raise_for_status()
-

benchmark/parse_log.py

@@ -17,6 +17,7 @@ def parse(file, parse_times = PARSE_FULL):
     commit = None
     times = None
     for line in file:
+        line = line.strip()
         # next commit?
         m = commit_re.match(line)
         if m is not None:
@@ -40,6 +41,7 @@ def parse(file, parse_times = PARSE_FULL):
                     times[name] = time
             continue
         # nothing else we know about, ignore
+        print("Ignoring line",line)
     # end of file. previous commit, if any, is done now.
     if commit is not None:
         yield Result(commit, times)

theories/heap_lang/proofmode.v

@@ -69,7 +69,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       |apply _                        (* IntoLaters *)
       |wp_expr_simpl_subst; try wp_value_head (* new goal *)
       ])
-    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
@@ -79,7 +79,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       |try fast_done                  (* The pure condition for PureExec *)
       |wp_expr_simpl_subst; try wp_value_head (* new goal *)
       ])
-    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
   | _ => fail "wp_pure: not a 'wp'"
   end.
 

theories/proofmode/coq_tactics.v

@@ -99,7 +99,7 @@ Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
 
 Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  if eqb p q then envs_simple_replace i p Γ Δ
+  if Bool.eqb p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete true i p Δ).
 
 Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
@@ -332,7 +332,7 @@ Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
   of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
-  rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
+  rewrite /envs_replace; destruct (Bool.eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
   - apply envs_app_sound.
 Qed.