aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Expand)AuthorAgeFilesLines
* Increasing required OCaml version (Pervasives <-> Stdlib module renaming)Cyril SIX2021-05-041-2/+2
* Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+1
* begin implementing selectDavid Monniaux2021-02-021-0/+1
* fix Makefile / configureDavid Monniaux2021-02-011-0/+6
* directory postpass_libSylvain Boulmé2021-01-071-3/+3
* recreate abstractbb/Sylvain Boulmé2021-01-071-2/+2
* cleaningSylvain Boulmé2021-01-071-1/+1
* Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into aarch64-p...Léo Gourdin2020-12-201-2/+2
|\
| * intermediatet commit before builtinsLéo Gourdin2020-12-161-1/+1
| * Removing the PseudoAsm IRLéo Gourdin2020-12-131-2/+2
* | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-0/+1
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-75/+80
|\ \ | |/ |/|
| * upgrade kvx backend to coq.8.12.2Sylvain Boulmé2020-12-161-1/+1
| * Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-3/+2
| |\
| * \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-73/+80
| |\ \
| | * | Support Coq 8.12.1Xavier Leroy2020-11-141-2/+2
| | * | Support Cygwin 64 bitsXavier Leroy2020-10-051-0/+13
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-42/+44
| | * | Remove support for x86-32 under macOSXavier Leroy2020-07-291-24/+0
| | * | Revised detection of menhirLib directory, continued (#365)Xavier Leroy2020-07-151-4/+4
| | * | Bytecode-only build (#243)Xavier Leroy2020-07-071-3/+14
| | * | Revised detection of menhirLib directory (#248)Xavier Leroy2020-07-071-2/+6
| | * | Preliminary support for Coq 8.12Xavier Leroy2020-06-211-3/+3
| | * | Compatibility with coq 8.11.2Bernhard Schommer2020-06-081-1/+1
| | * | Support for coq 8.11.1.Bernhard Schommer2020-04-201-2/+2
* | | | Ocaml peephole oracle and array datastruct instead of listsLéo Gourdin2020-12-081-1/+1
* | | | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-041-1/+1
* | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-271-8/+6
|\ \ \ \ | | |_|/ | |/| |
| * | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-3/+1
| * | | Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-161-2/+4
| |\ \ \
| | * | | just missing OpWeights for AARCH64David Monniaux2020-09-161-0/+1
| | * | | starting to move common filesDavid Monniaux2020-09-161-2/+3
| * | | | refactoring of RTLpathSE_impl.v (split with _simu_specs)Sylvain Boulmé2020-10-131-1/+1
| |/ / /
| * | | Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash...David Monniaux2020-07-301-1/+1
| |\| |
| * | | Coq 8.11.2David Monniaux2020-07-241-1/+1
| * | | start a junk implementation of the pre-pass verifierSylvain Boulmé2020-07-221-1/+1
| * | | remove useless (and unprovable) lemmas on completeness of the refinementSylvain Boulmé2020-07-021-1/+1
| * | | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-281-16/+17
| |\ \ \
| * | | | allow Coq 8.11.1David Monniaux2020-04-131-1/+1
| * | | | [BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSECyril SIX2020-04-101-18/+13
| |\ \ \ \
| * | | | | Compatibility Coq 8.11.0Cyril SIX2020-04-101-1/+1
| * | | | | RTLpath: removing some admits.Sylvain Boulmé2020-01-041-1/+1
| * | | | | RTLpath: semantical properties of liveness (with most of proofs)Sylvain Boulmé2019-12-261-1/+1
| * | | | | RTLpathLivegen: proof of preservationSylvain Boulmé2019-12-241-1/+1
| * | | | | experiments a definition of "path_simu"Sylvain Boulmé2019-11-141-1/+1
| * | | | | fix configure broken by mergeSylvain Boulmé2019-10-171-3/+0
| * | | | | Merge branch 'mppa-work' into RTLpathSylvain Boulmé2019-10-161-2/+4
| |\ \ \ \ \
| * \ \ \ \ \ Merge branch 'mppa-work' into RTLpathSylvain Boulmé2019-10-161-2/+2
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge tag 'v3.6_mppa_2019-09-20' into RTLpathDavid Monniaux2019-09-201-4/+34
| |\ \ \ \ \ \ \
| | * \ \ \ \ \ \ Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workv3.6_mppa_2019-09-20David Monniaux2019-09-201-4/+33
| | |\ \ \ \ \ \ \
generated by cgit (git 2.34.1) at 2024-06-02 23:08:26 +0000