Commits · df82ed633aab5d83f254d87ffc24c653173fdc63 · AVA / FloVer

27 Apr, 2018 1 commit
- Disable coq8.8.0 checking until branch is merged · df82ed63
  Heiko Becker authored Apr 27, 2018
  
  df82ed63
26 Apr, 2018 1 commit
- Remove unused conditional from CI script as it should always be true · f69f815e
  Heiko Becker authored Apr 26, 2018
  
  f69f815e
25 Apr, 2018 4 commits
- Use correct version number for Flocq · cfc1a50e
  Heiko Becker authored Apr 25, 2018
  
  cfc1a50e
- Update coq to 8.8 · bc362cfc
  Heiko Becker authored Apr 25, 2018
  
  bc362cfc
- Update .gitlab-ci.yml · cffe703c
  Heiko Becker authored Apr 25, 2018
  
  cffe703c
- Next step for reworked ci, now the Dockerimage must be rebuild · 8cf59d34
  Heiko Becker authored Apr 25, 2018
  
  8cf59d34
24 Apr, 2018 1 commit
- Next iteration on ci script · ddafa605
  Heiko Becker authored Apr 24, 2018
  
  ddafa605
23 Apr, 2018 3 commits
- More script fixes · fb68d0ce
  Heiko Becker authored Apr 23, 2018
  
  fb68d0ce
- Fix typo · 1922e1c4
  Heiko Becker authored Apr 23, 2018
  
  1922e1c4
- Remove not useful stuff from dockerfile and start updating ci script for HOL4 · 0cc50396
  Heiko Becker authored Apr 23, 2018
  
  0cc50396
20 Apr, 2018 3 commits
- Merge branch 'master' into fixed_point_hol4 · 215ffe0f
  Heiko Becker authored Apr 20, 2018
  
  215ffe0f
- Update parser and lexer · 3637e1bb
  Heiko Becker authored Apr 20, 2018
  
  3637e1bb
- Add fixed-point precision to HOL4, fix minor bug in configure script · 3d6185b5
  Heiko Becker authored Apr 20, 2018
  
  3d6185b5
18 Apr, 2018 6 commits
- Next fix... · 9c1261ae
  Heiko Becker authored Apr 18, 2018
  
  9c1261ae
- Final bug fix? · 60da67c9
  Heiko Becker authored Apr 18, 2018
  
  60da67c9
- Fix another number bug in bash scripts · 32d50f08
  Heiko Becker authored Apr 18, 2018
  
  32d50f08
- Next bug fix · 262be4d3
  Heiko Becker authored Apr 18, 2018
  
  262be4d3
- Fix some submodule cloning bugs in CI and update CI script for HOL4 · b1ba3071
  Heiko Becker authored Apr 18, 2018
  
  b1ba3071
- Make ci check for updated HOL4 · eafb3aaf
  Heiko Becker authored Apr 18, 2018
  
  eafb3aaf
17 Apr, 2018 4 commits
- Merge branch 'master' into fixed_point_hol4 · 2dd19d8d
  Heiko Becker authored Apr 17, 2018
  
  2dd19d8d
- Update CakeML to the latest compiling state · 67de6c46
  Heiko Becker authored Apr 17, 2018
  
  67de6c46
- Add a pre-commit hook that verifies that HOLCOMMIT and HOLDIRs commit hash coincide · 2611a9f2
  Heiko Becker authored Apr 17, 2018
  
  2611a9f2
- Update Dockerfile to not depend on HOLCOMMIT variable in the file · 306bb00f
  Heiko Becker authored Apr 17, 2018
  
  306bb00f
09 Apr, 2018 5 commits
- Merge branch 'WIP_fix_broken_Flover_compute' into 'master' · 18e07778
  Heiko Becker authored Apr 09, 2018
```
Fix Flover compute handling of new notations.

See merge request AVA/FloVer!3
```
  18e07778
- Fix proofs broken by new syntax for option bindings · 285be625
  Heiko Becker authored Apr 09, 2018
  
  285be625
- Merge branch 'option_bind' into 'WIP_fix_broken_Flover_compute' · be61af35
  Heiko Becker authored Apr 09, 2018
```
Rename 'optionLift' with 'optionBind'

See merge request AVA/FloVer!2
```
  be61af35
- Start resolving compilation issues · 0a00766a
  Nikita Zyuzin authored Apr 09, 2018
  
  0a00766a
- Rename 'optionLift' with 'optionBind' · 37d050e2
  Nikita Zyuzin authored Apr 06, 2018
```
Introduce useful notations for it
```
  37d050e2
04 Apr, 2018 2 commits
- Merge branch 'fixed_point_checking' into 'master' · ddc04b14
  Heiko Becker authored Apr 04, 2018
```
Add fixed-point checking to FloVer's coq development

See merge request AVA/FloVer!1
```
  ddc04b14
- Add explanation of isMorePrecise for fixed-points, rename M0 into REAL and... · 40a32997
  Heiko Becker authored Apr 04, 2018
```
Add explanation of isMorePrecise for fixed-points, rename M0 into REAL and remove unused import from Expressions.v
```
  40a32997
29 Mar, 2018 9 commits
- WIP: Start working on HOL4 fixed-point checking · c7ff0b5e
  Heiko Becker authored Mar 29, 2018
  
  c7ff0b5e
- WIP:Fix broken FP range calculation · 8a64fbf4
  Heiko Becker authored Mar 29, 2018
  
  8a64fbf4
- Fix theorem placement, broken by refactoring · 6bc1a0dd
  Heiko Becker authored Mar 29, 2018
  
  6bc1a0dd
- Merge branch 'master' into fixed_point_checking · 9894803f
  Heiko Becker authored Mar 29, 2018
  
  9894803f
- Merge branch 'master' into fixed_point_checking · e777bccf
  Heiko Becker authored Mar 29, 2018
  
  e777bccf
- Update .gitlab-ci.yml to run on anything that is not a "WIP:" commit · 4c0b242a
  Heiko Becker authored Mar 29, 2018
  
  4c0b242a
- Add a simple regression test for fixed-point checking · 69ba85c7
  Heiko Becker authored Mar 29, 2018
  
  69ba85c7
- Push changed Ltacs file forgotten by last commit · 124cb845
  Heiko Becker authored Mar 29, 2018
  
  124cb845
- Add Fixed-Point checking to FloVer in Coq. · da70f298
  Heiko Becker authored Mar 29, 2018
```
Refactor error computation in semantics into separate function/Proposition
to be able to differentiate between truncation and rounding-to-nearest error.
```
  da70f298
12 Mar, 2018 1 commit
- Fix type renaming also for regression tests · dee127fa
  Heiko Becker authored Mar 12, 2018
  
  dee127fa