1. 03 Oct, 2011 3 commits
    • Guillaume Melquiond's avatar
      Started a realization of real.real. · 72b12557
      Guillaume Melquiond authored
      This is just a proof of concept, since most definitions should just be
      notations for the realization to be user-friendly. Moreover, the format of
      the file will presumably evolve, if only for some information to properly
      update it when the theories change.
      
      Remark about the theory : Lemma mul_assoc_div has an extraneous hypothesis.
      Indeed, as long as inverse is a total function, this lemma is an immediate
      consequence of multiplication associativity.
      72b12557
    • Asma Tafat's avatar
      Latex statistics · b41ae8ca
      Asma Tafat authored
      b41ae8ca
    • Asma Tafat's avatar
      Latex statistics · b991de54
      Asma Tafat authored
      b991de54
  2. 01 Oct, 2011 1 commit
  3. 30 Sep, 2011 4 commits
    • Andrei Paskevich's avatar
      add the option --realize to Main · 9ab0704b
      Andrei Paskevich authored
      How to use it:
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real -o .
      
              produces Real.v in the current directory
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real
      
              produces real/Real.v in the loadpath near real.why
              (the directory "real" must exist)
      
      If a realization file is already there, it is passed to
      the printer in order to preserve the proofs.
      
      Instead of -D <driver_file>, you can use -P <prover>,
      if that prover uses a corresponding driver. However,
      the prover itself is not used.
      
      You can only realize theories from the loadpath.
      
      At the moment, coq-realize.drv is the only driver
      capable to realize theories in some sensible way.
      For any other driver, the results may be funny.
      
      Realization of WhyML modules is not possible so far.
      
      Realization may break if you directories and filenames
      contain non-alphanumeric symbols.
      
      The whole thing is in very preliminary stage.
      Use with caution.
      9ab0704b
    • Andrei Paskevich's avatar
      30dda877
    • Andrei Paskevich's avatar
      rename Env.create_env_of_loadpath to Env.create_env · b92e64bc
      Andrei Paskevich authored
      also add Env.get_loadpath to use for Coq realisation
      b92e64bc
    • MARCHE Claude's avatar
      alternative timeout regexp for vampire · 75e1e522
      MARCHE Claude authored
      75e1e522
  4. 29 Sep, 2011 7 commits
  5. 28 Sep, 2011 7 commits
  6. 27 Sep, 2011 2 commits
  7. 26 Sep, 2011 7 commits
  8. 25 Sep, 2011 1 commit
  9. 24 Sep, 2011 3 commits
    • Guillaume Melquiond's avatar
      Keep track of "ITP" provers and avoid running such provers on unedited proofs. · 406f058e
      Guillaume Melquiond authored
      When the user wants to write a Coq proof, she needs to run Coq on the goal,
      wait five seconds for it to fail (it will fail, otherwise there is no point
      in running Coq on this goal: another prover would have succeeded already),
      and finally edit it. This is a waste of time. So goals run with an
      interactive prover are now marked as unknown until their file is edited.
      
      Interactive provers could have been detected by a nonempty "editor" string,
      but there are interactive provers that don't have dedicated editors, and
      there might be automated provers with dedicated user interfaces. So a new
      field was added to prover descriptions.
      
      TODO: actually run the editor when there is only one selected goal,
      rather than keeping the current three-click method of editing proofs.
      406f058e
    • MARCHE Claude's avatar
      Improved monitoring of running proofs · 841b97b2
      MARCHE Claude authored
      841b97b2
    • MARCHE Claude's avatar
      39918c7e
  10. 23 Sep, 2011 4 commits
  11. 22 Sep, 2011 1 commit
    • Guillaume Melquiond's avatar
      Fix incorrect usage of t_fold. · cb5c96e7
      Guillaume Melquiond authored
      t_fold already iters on the subterms of a term, so calling t_fold on a
      subterm actually iters over grandchildren of the term, which may well be
      under a quantifier. So t_fold should be called on the term itself.
      
      This explains why the transformation was trying to create declarations with
      unbounded variables.
      cb5c96e7