Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

  1. 29 Oct, 2013 3 commits
    • Andrei Paskevich's avatar
      Term: do not store t_vars in terms · 7abeba05
      Andrei Paskevich authored
      we still keep bv_vars in the binders, so calculating the set
      of free variables only has to descend to the topmost binders.
      The difference on an example from BWare is quite striking:
      
      /usr/bin/time why3-replayer : with t_vars
      
      505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k
      
      /usr/bin/time why3-replayer : without t_vars
      
      242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k
      
      Not only we take 2/3 of memory, but we also gain in speed (less work
      for the GC, most probably).
      
      This patch should be tested on big WhyML examples,
      since src/whyml/mlw_*.ml are big users of t_vars.
      
      Thanks to Guillaume for the suggestion.
      7abeba05
    • Andrei Paskevich's avatar
    • MARCHE Claude's avatar
      Fix pb with bench on Coq tactic · a39b8c95
      MARCHE Claude authored
      a39b8c95
  2. 28 Oct, 2013 6 commits
  3. 22 Oct, 2013 5 commits
  4. 21 Oct, 2013 2 commits
  5. 19 Oct, 2013 1 commit
  6. 18 Oct, 2013 4 commits
  7. 17 Oct, 2013 2 commits
  8. 16 Oct, 2013 9 commits
  9. 11 Oct, 2013 4 commits
  10. 10 Oct, 2013 4 commits