Commits · 0ec854159b693a6098587c336e79aca67a915187 · AVA / FloVer

24 Aug, 2018 5 commits
- Make script to build binaries executable · 0ec85415
  Heiko Becker authored Aug 24, 2018
  
  0ec85415
- Update gitlab ci config to run the binary phase · 19822e6d
  Heiko Becker authored Aug 24, 2018
  
  19822e6d
- Merge branch 'master' of gitlab.mpi-sws.org:AVA/FloVer · 3868698c
  Heiko Becker authored Aug 24, 2018
  
  3868698c
- Rework CI infrastructure a bit to make the scripts account for caching · 7e05f873
  Heiko Becker authored Aug 24, 2018
```
Coq CI script fails early when 8.7.2  compilation breaks
HOL4 CI script does not build binaries anymore, this is done by ci-binary.sh
ci-binary.sh can be used to build both Coq and HOl4 binaries in a separate pipeline
```
  7e05f873
- Update .gitlab-ci.yml to cache HOL4 state · aae0ebed
  Heiko Becker authored Aug 24, 2018
  
  aae0ebed
22 Aug, 2018 1 commit
- Adapt simple regression test in Coq · 9ac65923
  Heiko Becker authored Aug 22, 2018
  
  9ac65923
20 Aug, 2018 1 commit
- Fix bug in environment parser · 92b5700e
  Heiko Becker authored Aug 20, 2018
  
  92b5700e
19 Aug, 2018 4 commits
- Merge branch 'master' of gitlab.mpi-sws.org:AVA/FloVer · 28b09555
  Heiko Becker authored Aug 19, 2018
  
  28b09555
- Update script to with correct paths · c3247be5
  Heiko Becker authored Aug 19, 2018
  
  c3247be5
- Readd mixed-precision maps · 8ff697e3
  Heiko Becker authored Aug 19, 2018
  
  8ff697e3
- Update .gitlab-ci.yml to not make artifacts expire · 2dbeed8b
  Heiko Becker authored Aug 19, 2018
  
  2dbeed8b
18 Aug, 2018 3 commits
- Merge branch 'reworked_type_validator' into 'master' · b16dcdea
  Heiko Becker authored Aug 18, 2018
```
Finish reworking the type inferencer

Closes #7

See merge request AVA/FloVer!13
```
  b16dcdea
- Fix IEEE_connection Script · 92854d7c
  Heiko Becker authored Aug 18, 2018
  
  92854d7c
- Make ci more verbose to debug · 5f55f541
  Heiko Becker authored Aug 18, 2018
  
  5f55f541
17 Aug, 2018 3 commits
- Merge remote-tracking branch 'origin/master' into reworked_type_validator · 1b9d5130
  Heiko Becker authored Aug 17, 2018
  
  1b9d5130
- Merge branch 'reworked_type_validator' of gitlab.mpi-sws.org:AVA/FloVer into... · e29df18b
  Heiko Becker authored Aug 17, 2018
```
Merge branch 'reworked_type_validator' of gitlab.mpi-sws.org:AVA/FloVer into reworked_type_validator
```
  e29df18b
- Fix bug in translationScript and fforward CakeML · 69e60d78
  Heiko Becker authored Aug 17, 2018
  
  69e60d78
16 Aug, 2018 3 commits
- Simplify Coq files more · 53eb2e1c
  Heiko Becker authored Aug 16, 2018
  
  53eb2e1c
- Fix compilation error in IEEE_connection.v · cb3b7782
  Heiko Becker authored Aug 16, 2018
  
  cb3b7782
- minor style changes in Coq dev and finish porting in HOL4 · 96bc2e7e
  Heiko Becker authored Aug 16, 2018
  
  96bc2e7e
15 Aug, 2018 1 commit
- Finish translation with CakeML, prove IEEE connection for expressions · 858e91ae
  Heiko Becker authored Aug 15, 2018
  
  858e91ae
14 Aug, 2018 4 commits
- Port CC functions · 316f0b15
  Heiko Becker authored Aug 14, 2018
  
  316f0b15
- Port FPRangeValidator · 58bb46dc
  Heiko Becker authored Aug 14, 2018
  
  58bb46dc
- Finish Error Validation · a5076909
  Heiko Becker authored Aug 14, 2018
  
  a5076909
- Some cleanup and progress on Error Validator soundness · dac0edc4
  Heiko Becker authored Aug 14, 2018
  
  dac0edc4
13 Aug, 2018 1 commit
- WIP: Next step for IV validation · 9325d322
  Heiko Becker authored Aug 13, 2018
  
  9325d322
10 Aug, 2018 1 commit
- WIP for Interval Validation · 7b1808b0
  Heiko Becker authored Aug 10, 2018
  
  7b1808b0
09 Aug, 2018 1 commit
- Port ErrorBoundsScript to new semantics · 2dea97d6
  Heiko Becker authored Aug 09, 2018
  
  2dea97d6
08 Aug, 2018 1 commit
- Implement and prove correct new type inferencer in HOL4 · 2e3a7e7e
  Heiko Becker authored Aug 08, 2018
  
  2e3a7e7e
02 Aug, 2018 3 commits
- Merge branch 'reworked_type_validator' into 'master' · 6f1ffdcc
  Heiko Becker authored Aug 02, 2018
```
Rework Coq type validator

See merge request AVA/FloVer!12
```
  6f1ffdcc
- Fix remaining admits · 4ccb040c
  Heiko Becker authored Aug 02, 2018
  
  4ccb040c
- Fix IEEE connection and AA validators · 4d4ab82d
  Heiko Becker authored Aug 02, 2018
  
  4d4ab82d
31 Jul, 2018 2 commits
- Fix overall soundness theorem and FPRangevalidator soundness · 7e8898d7
  Heiko Becker authored Jul 31, 2018
  
  7e8898d7
- Fix soundness proof for roundoff error valdator · e320513e
  Heiko Becker authored Jul 31, 2018
  
  e320513e
30 Jul, 2018 1 commit
- Rename Lemma in ExpressionsSemantics and fix assumptions for abstract bound lemmas · c056a2d9
  Heiko Becker authored Jul 30, 2018
  
  c056a2d9
27 Jul, 2018 3 commits
- Change toRTMap to toRExpMap to make function purpose clearer, fix broken... · ebc6d460
  Heiko Becker authored Jul 27, 2018
```
Change toRTMap to toRExpMap to make function purpose clearer, fix broken proofs up until ErrorBounds.v
```
  ebc6d460
- Fix admits in RealRangeArith · 61a5e249
  Heiko Becker authored Jul 27, 2018
  
  61a5e249
- Fix admits in ExpressionSemantics.v · 2fe03457
  Heiko Becker authored Jul 27, 2018
  
  2fe03457
26 Jul, 2018 2 commits
- Remove unnecessary print · 5d673f75
  Heiko Becker authored Jul 26, 2018
  
  5d673f75
- Finish proving correctness of new type computation · ea902e6d
  Heiko Becker authored Jul 26, 2018
  
  ea902e6d