1. 11 Jul, 2019 1 commit
  2. 04 Jul, 2019 1 commit
  3. 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
  4. 13 Jun, 2019 1 commit
  5. 05 Jun, 2019 2 commits
  6. 29 May, 2019 1 commit
  7. 13 May, 2019 1 commit
  8. 04 Apr, 2019 1 commit
    • Sylvain Dailler's avatar
      Add experimental coq realization for Fset and other Set theory · c5d97975
      Sylvain Dailler authored
      The underlying datastructure is not satisfying nor are the proofs but at
      least there is a quick simple realization. It uses ClassicalEpsilon axioms
      such as excluded middle, indefinite_description etc...
      Some theory realizations are very far from reality because the axiom
      characterization is small.
      c5d97975
  9. 29 Mar, 2019 1 commit
  10. 28 Mar, 2019 1 commit
  11. 04 Mar, 2019 1 commit
  12. 11 Feb, 2019 1 commit
  13. 07 Feb, 2019 1 commit
  14. 17 Dec, 2018 2 commits
  15. 05 Dec, 2018 1 commit
    • Sylvain Dailler's avatar
      ce: support for if-branching · b0ef7adf
      Sylvain Dailler authored
      This adds introduce_premises as a counterexample transformation (to
      introduce possible exists quantifications) and add attributes that are
      tagged with the special branch_id= to variables directly near it.
      b0ef7adf
  16. 27 Nov, 2018 2 commits
  17. 08 Nov, 2018 1 commit
  18. 22 Oct, 2018 1 commit
  19. 14 Sep, 2018 1 commit
  20. 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
  21. 29 Aug, 2018 1 commit
  22. 24 Aug, 2018 1 commit
    • Andrei Paskevich's avatar
      Subst: avoid selecting polymorphic symbols and constructors · f542a3e4
      Andrei Paskevich authored
      Also, add an .mli file and export the relevant functions.
      
      Also, provide a variant of "split_vc" in introduction.ml
      which uses subst over introduced non-model constants instead
      of "simplify_trivial_quantification". This is more efficient
      and produces better results. Commented at the moment because
      of session breakage.
      f542a3e4
  23. 20 Aug, 2018 2 commits
  24. 14 Aug, 2018 1 commit
  25. 25 Jul, 2018 1 commit
  26. 11 Jul, 2018 1 commit
    • Mário Pereira's avatar
      Why3 "bootstrap": · 0da5f41e
      Mário Pereira authored
      The code in file /src/util/pqueue.ml has been extracted from a Why3 proof,
      and is now a correct-by-construction OCaml code. This file depends on the Vector
      module, which is also an OCaml implementation extracted from another Why3 proof.
      The proofs can be found in /examples/util/
      
      This is the result of Aymeric Walch bachelor internship.
      0da5f41e
  27. 06 Jul, 2018 1 commit
  28. 04 Jul, 2018 1 commit
  29. 02 Jul, 2018 1 commit
  30. 28 Jun, 2018 1 commit
  31. 25 Jun, 2018 1 commit
  32. 24 Jun, 2018 1 commit
  33. 23 Jun, 2018 1 commit
  34. 22 Jun, 2018 2 commits
  35. 21 Jun, 2018 1 commit
    • Johannes Kanig's avatar
      R531-011 implement killing of tasks · 07b60cd3
      Johannes Kanig authored
      The why3server supports the "interrupt" command which removes a task.
      But until now, the server didn't actually kill any already running
      processes. This is now implemented.
      
      Background is that I plan some refactorings which may make use of the
      "interrupt" command, so I want it to work properly.
      
      This new code is untested on windows, because no client code actually
      uses the interrupt command in SPARK. But I tested that it doesn't cause
      regressions. It will be later tested by the new code I intend to write.
      
      *server-unix.c
      *server-win.c
      (overall): outsource some little code to new proc unit
      (handle_msg): actually kill processes
      
      * proc.c - new file
      (os_kill): new platform-dependent function to kill a process by pid
      (init_process_list): new function to init the process list
      (kill_processes): new function to kill processes from process list with
        a certain key
      (free_process): release memory held by a process record
      
      Change-Id: I7238578061c65883423f8ec538d79d9de3fb717b
      (cherry picked from commit b17873a181ff56abda9d09bc8d10c29ba036c019)
      07b60cd3