1. 17 Dec, 2018 2 commits
  2. 04 Sep, 2018 1 commit
  3. 29 Aug, 2018 1 commit
  4. 20 Aug, 2018 1 commit
  5. 08 Jun, 2018 1 commit
    • Guillaume Melquiond's avatar
      Make menhirLib mandatory (fix issue #118). · 87c856ea
      Guillaume Melquiond authored
      Menhir 20151112 can, in fact, be used to compile Why3. The actual issue
      was that the error reporting module depends on Menhir's table-based
      backend, which requires menhirLib. So, the latter is no longer an optional
      dependency.
      87c856ea
  6. 29 May, 2018 1 commit
  7. 27 May, 2018 1 commit
    • Guillaume Melquiond's avatar
      Check whether ocamlfind might have returned the actual location of nums.cma. · 31ad65d5
      Guillaume Melquiond authored
      The standard install location of the num library is $OCAMLLIB. Thus, the
      answer of ocamlfind cannot generally be trusted since it returns the
      location of the META file. Yet, on Arch Linux, nums.cma is actually stored
      next to its META file, for some reason. So, this commit makes configure
      try this location before falling back to the standard one.
      31ad65d5
  8. 24 May, 2018 1 commit
    • Guillaume Melquiond's avatar
      Drop support for Coq 8.4. · 5f0df6ba
      Guillaume Melquiond authored
      Generated statements were actually ill-formed, since Coq 8.4 sometimes
      interprets "A -> B <-> C" as "(A -> B) <-> C". (This bug was fixed in 8.5.)
      We could print additional parentheses to work around the issue, but it is
      about time we drop support for Coq 8.4 anyway.
      5f0df6ba
  9. 23 May, 2018 1 commit
  10. 22 May, 2018 1 commit
  11. 16 May, 2018 6 commits
  12. 26 Mar, 2018 1 commit
  13. 23 Mar, 2018 1 commit
  14. 22 Mar, 2018 2 commits
  15. 20 Mar, 2018 2 commits
  16. 09 Feb, 2018 2 commits
  17. 07 Feb, 2018 1 commit
  18. 05 Feb, 2018 1 commit
  19. 02 Feb, 2018 1 commit
  20. 11 Jan, 2018 1 commit
  21. 11 Dec, 2017 1 commit
    • Sylvain Dailler's avatar
      Update configure and regtests / nightly-build so that realization are · 190492a8
      Sylvain Dailler authored
      generated again.
      
      * Makefile.in
      Realizations for isabelle are generated even if Isabelle is not installed.
      The .thy file are checked only if isabelle is installed. This allows us
      to treat it as with coq and be able to detect changes in realizations
      with a script.
      Dont erase xml generated file during clean.
      
      * configure.in
      Changed the configure to always generate a default isabelle version (set
      to 2017) for generation of the realization driver (needed even when no
      isablle support is given).
      
      * examples/regtests.sh
      Adding option --check-realization and --only-realization which add a test
      the compares the output of the new realization compared to the one
      recorded. It complains if they are different forcing the user to update the
      realization files.
      
      * lib/isabelle/*
      Adding xml files corresponding to generated realization for Isabelle. This
      allows for the abovementionned script to work even if Isabelle is not
      installed (which is the case for most people editing theories).
      
      * examples/nightly-bench.sh
      Add the option for realization check
      
      * misc/ci-bench
      Calls the test for realization
      
      Conflicts:
      	examples/regtests.sh
      190492a8
  22. 22 Nov, 2017 1 commit
  23. 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
  24. 20 Oct, 2017 1 commit
  25. 16 Oct, 2017 1 commit
  26. 13 Oct, 2017 1 commit
  27. 09 Oct, 2017 1 commit
  28. 03 Oct, 2017 1 commit
  29. 26 Sep, 2017 2 commits
  30. 12 Sep, 2017 1 commit