1. 05 May, 2020 1 commit
  2. 05 Jul, 2019 1 commit
    • Jacques-Henri Jourdan's avatar
      New parser based on new version of the Coq backend of Menhir (#276) · 998f3c5f
      Jacques-Henri Jourdan authored
      What's new:
      1. A rewrite of the Coq interpreter of Menhir automaton, with
         dependent types removing the need for runtime checks for the
         well-formedness of the LR stack. This seem to cause some speedup on
         the parsing time (~10% for lexing + parsing).
      2. Thanks to 1., it is now possible to avoid the use of int31 for
         comparing symbols: Since this is only used for validation,
         positives are enough.
      3. Speedup of Validation: on my machine, the time needed for compiling
         Parser.v goes from about 2 minutes to about 1 minute. This seem to
         be related to a performance bug in the completeness validator and
         to the use of positive instead of int31.
      3. Menhir now generates a dedicated inductive type for
         (semantic-value-carrying) tokens (in addition to the already
         existing inductive type for (non-semantic-value-carrying)
         terminals. The end result is that the OCaml support code for the
         parser no longer contain calls to Obj.magic. The bad side of this
         change is that the formal specification of the parser is perhaps
         harder to read.
      4. The parser and its library are now free of axioms (I used to use
         axiom K and proof irrelevance for easing proofs involving dependent
      5. Use of a dedicated custom negative coinductive type for the input
         stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
         positive coinductive type, which are now deprecated by Coq.
      6. The fuel of the parser is now specified using its logarithm instead
         of its actual value. This makes it possible to give large fuel
         values instead of using the `let rec fuel = S fuel` hack.
      7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
      The corresponding changes in Menhir have been released as part of
      version 20190626. The `MenhirLib` directory is identical to the
      content of the `src` directory of the corresponding `coq-menhirlib`
      opam package except that:
         - In order to try to make CompCert compatible with several Menhir
           versions without updates, we do not check the version of menhir
           is compatible with the version of coq-menhirlib. Hence the
           `Version.v` file is not present in CompCert's copy.
         - Build-system related files have been removed.
  3. 05 Jan, 2018 1 commit
    • Xavier Leroy's avatar
      Resynchronize the LICENSE file and the license headers in individual files (#45) · 9ccb6a24
      Xavier Leroy authored
      Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file.  OVer the years those two markings got inconsistent.
      This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
      Some build-related files were dual-licensed but some others were not.  Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
      Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed.  Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
      which is not in lib/
  4. 14 Feb, 2017 1 commit
  5. 30 Jun, 2016 1 commit
    • Xavier Leroy's avatar
      common/Determinism.v: dual-license with GPL · db2445b3
      Xavier Leroy authored
      There was no good reason why Determinism.v was the only file in common/ that was not dual-licensed (GPL + noncommercial).  Plus, it simplifies the wording of the LICENSE file.
  6. 28 Jun, 2016 1 commit
  7. 19 Feb, 2016 1 commit
  8. 26 Jun, 2015 1 commit
  9. 12 Jun, 2015 1 commit
  10. 29 Apr, 2014 1 commit
  11. 21 Feb, 2014 1 commit
  12. 17 Jun, 2013 2 commits
  13. 09 Jan, 2013 1 commit
  14. 08 Oct, 2012 1 commit
  15. 13 Jul, 2012 1 commit
  16. 28 Jun, 2012 1 commit
  17. 11 Mar, 2012 1 commit
  18. 23 Aug, 2011 1 commit
  19. 27 Oct, 2010 1 commit
  20. 03 Mar, 2010 1 commit
  21. 29 Mar, 2009 1 commit
  22. 05 Jan, 2009 1 commit
  23. 28 Jan, 2008 1 commit
  24. 27 Jan, 2008 1 commit