1. 04 Oct, 2019 1 commit
  2. 19 Sep, 2019 2 commits
  3. 04 Jul, 2019 1 commit
  4. 27 Jun, 2019 1 commit
  5. 21 Jun, 2019 1 commit
    • MARCHE Claude's avatar
      Remove all usages of obsolete library why3extract.cma · 1f766d25
      MARCHE Claude authored
      Two of the three examples which are extracted to ocaml code and then to
      javascript are not working, but they were broken since the new extraction
      which is bound to the use of Zarith and not Num. They should be
      repaired when js_of_ocaml supports Zarith
      1f766d25
  6. 17 May, 2019 1 commit
  7. 17 Dec, 2018 1 commit
  8. 11 Sep, 2018 1 commit
    • Guillaume Melquiond's avatar
      Remove handcrafted error messages (fix issues #150 and #172). · ce21b6c1
      Guillaume Melquiond authored
      Short story: it was a source of bugs, there was only one handcrafted
      message over 650, and, to quote François Pottier, "you seem to have
      misunderstood what the various commands do".
      
      Long story: the proper steps to update the error messages after modifying
      the parser are
      
      1. update the old states with --update-errors
      2. generate the new states with --list-errors
      3. compare the old and new states with --compare-errors
      4. manually reconcile the differences between the old and new states
      5. write error messages for the new states
      6. add %on_error_reduce and go back to step 1, if step 5 is too hard
      7. check that the error messages for the old states are still meaningful
      8. check that the set of states is both correct (--compile-errors) and
         complete (--compare-errors)
      
      We were doing only step 1 and half of step 8. Doing the other half of
      step 8 would have prevented issue #172 from occurring. But that would have
      meant doing step 4 after each parser modification, which was never done.
      Note that step 2 is so expensive that it is impossible to perform step 8
      during continuous integration.
      
      Given the work needed to update the error messages after a syntax change,
      I don't think we can reliably use them until WhyML no longer evolves.
      ce21b6c1
  9. 20 Aug, 2018 2 commits
  10. 18 Jun, 2018 1 commit
  11. 05 Jun, 2018 1 commit
  12. 01 Jun, 2018 1 commit
  13. 29 May, 2018 1 commit
  14. 25 May, 2018 1 commit
  15. 22 May, 2018 1 commit
  16. 16 May, 2018 1 commit
  17. 02 May, 2018 2 commits
  18. 12 Apr, 2018 1 commit
  19. 22 Mar, 2018 1 commit
  20. 15 Dec, 2017 1 commit
  21. 27 Nov, 2017 1 commit
  22. 12 Nov, 2017 1 commit
    • Guillaume Melquiond's avatar
      Detect whether coqtop.byte is present. · 4ff1dd2a
      Guillaume Melquiond authored
      It is needed for compiling the Coq tactic Why3.vo file when native
      compilation is disabled.
      
      This commit also avoid a potential race condition when Why3.vo was
      compiled with both the native and bytecode compilers.
      4ff1dd2a
  23. 08 Sep, 2017 1 commit
  24. 21 Jun, 2017 1 commit
  25. 23 May, 2017 1 commit
  26. 11 Apr, 2017 1 commit
  27. 05 Apr, 2017 1 commit
  28. 17 Mar, 2017 1 commit
  29. 20 Feb, 2017 1 commit
  30. 16 Feb, 2017 1 commit
  31. 11 Feb, 2017 1 commit
  32. 01 Feb, 2017 1 commit
  33. 31 Jan, 2017 2 commits
  34. 30 Jan, 2017 1 commit
  35. 29 Jan, 2017 2 commits