1. 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.
  2. 29 Mar, 2019 1 commit
  3. 28 Mar, 2019 1 commit
  4. 04 Mar, 2019 1 commit
  5. 11 Feb, 2019 1 commit
  6. 07 Feb, 2019 1 commit
  7. 17 Dec, 2018 2 commits
  8. 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.
  9. 27 Nov, 2018 2 commits
  10. 08 Nov, 2018 1 commit
  11. 22 Oct, 2018 1 commit
  12. 14 Sep, 2018 1 commit
  13. 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.
  14. 29 Aug, 2018 1 commit
  15. 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.
  16. 20 Aug, 2018 2 commits
  17. 14 Aug, 2018 1 commit
  18. 25 Jul, 2018 1 commit
  19. 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.
  20. 06 Jul, 2018 1 commit
  21. 04 Jul, 2018 1 commit
  22. 02 Jul, 2018 1 commit
  23. 28 Jun, 2018 1 commit
  24. 25 Jun, 2018 1 commit
  25. 24 Jun, 2018 1 commit
  26. 23 Jun, 2018 1 commit
  27. 22 Jun, 2018 2 commits
  28. 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.
      (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)
  29. 15 Jun, 2018 1 commit
  30. 08 Jun, 2018 3 commits
  31. 05 Jun, 2018 3 commits
  32. 04 Jun, 2018 1 commit