1. 23 Mar, 2018 1 commit
  2. 22 Mar, 2018 4 commits
  3. 21 Mar, 2018 2 commits
  4. 20 Mar, 2018 4 commits
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
      28cd7bdd
    • Guillaume Melquiond's avatar
      Fix typo. · df36c1d1
      Guillaume Melquiond authored
      df36c1d1
    • Guillaume Melquiond's avatar
      Improve installation targets (fixes issue #74). · a3b55e3d
      Guillaume Melquiond authored
      - The install and install-lib targets no longer remove existing files
        automatically. Use uninstall instead.
      - Dedicated install targets have been added: install-bin, install-data,
        install-emacs, install-bash, install-coq-tactic, install-coq,
        install-pvs, install-isabelle, install-framac.
      - Dedicated uninstall targets have been added: uninstall-bin,
        uninstall-lib, uninstall-emacs, uninstall-bash, uninstall-framac.
        (Other uninstall targets are covered by plain uninstall.)
      - The install target depends on all the install-* targets, except for
        install-lib.
      - The install and install-lib targets now work in local mode too. In that
        case, the install target does not depend on the install-bin and
        install-data targets.
      - The uninstall target depends on all the uninstall-* targets, including
        uninstall-lib. In local mode, dependencies on uninstall-bin and
        uninstall-data are ignored.
      a3b55e3d
  5. 09 Mar, 2018 1 commit
  6. 01 Mar, 2018 1 commit
  7. 06 Feb, 2018 1 commit
  8. 02 Feb, 2018 1 commit
  9. 17 Jan, 2018 2 commits
    • Jean-Christophe Filliatre's avatar
    • Stefan Berghofer's avatar
      Improved checking of realizations for Isabelle · 96f69b5e
      Stefan Berghofer authored
      Rather than using pre-generated files, the *.xml files describing the
      Why3 theories to be realized are generated again before compiling the
      corresponding Isabelle theories. Instead of the generated *.xml files,
      we use a file containing their hash values to detect changes in the
      realizations. Since there may be different realizations for different
      versions of Isabelle, we provide a file with hash values for every
      supported version of Isabelle. The files containing the hash values
      can be updated via the update-isabelle target.
      
      (cherry picked from commit 039e0f0a321c36ea3bea231e4376f5833cd2ad8a)
      96f69b5e
  10. 12 Jan, 2018 1 commit
  11. 11 Jan, 2018 1 commit
  12. 05 Jan, 2018 1 commit
  13. 26 Dec, 2017 3 commits
  14. 24 Dec, 2017 3 commits
  15. 22 Dec, 2017 1 commit
  16. 15 Dec, 2017 2 commits
  17. 11 Dec, 2017 4 commits
    • MARCHE Claude's avatar
      check realizations: generate them in a fresh temporary directory · f071fac7
      MARCHE Claude authored
      additional cosmetic changes
      f071fac7
    • MARCHE Claude's avatar
      cosmetic changes · 9a43c12a
      MARCHE Claude authored
      - do not erase Isabelle's XML files even in local mode
      
      - use realization*s* with an s everywhere
      9a43c12a
    • 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
    • Sylvain Dailler's avatar
      Adding induction_pr.ty_lex with arguments · d42da05f
      Sylvain Dailler authored
      * Makefile.in
      Reordered Lib_transform into makefile.
      
      * src/transform/ind_itp.ml
      Adding a dependant revert transformation
      
      * src/transform/ind_itp.mli
      Adding a transformation that does a dependant revert of a list of symbols.
      
      * src/transform/induction.ml
      Adding transformation induction_ty_lex and induction_on_hyp.
      
      * src/transform/induction_pr.ml
      induction_arg_pr and inversion_arg_pr added.
      d42da05f
  18. 08 Dec, 2017 1 commit
  19. 07 Dec, 2017 3 commits
  20. 29 Nov, 2017 1 commit
  21. 27 Nov, 2017 1 commit
  22. 17 Nov, 2017 1 commit