Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • Affine_Magnus protected
  • CI_test
  • FMCAD2018
  • FloVer2
  • SMT_Subdiv
  • fixpointdupsem
  • master default protected
  • rewriting_HOL4
  • FMCAD2018
9 results
Created with Raphaël 2.2.014Jul131236May25Apr10130Mar1624Feb23214Jan14Oct49Sep18Jun1710Mar98522Jan2119181223Jul1012May22Apr25Mar242319187Nov28Oct25181Jul17Jun1429May729Apr1110985432129Mar282726201514131211865128Feb2725222015141385129Jan272523221514119821Dec201817141211109765428Nov27262120191615141331Oct302423181612111098542128Sep27262524201918171413121110876543131Aug302928252423222019181716151413109876231Jul30272624201412116543211Jun9630May252423212019181716151412111098765432130Apr27262524232120191817109654329Mar282726242322212016151413129Make CI more stringent to see error messages properlymastermasterUse OLD_REAL_ASM_ARITH_TAC in FpRangeValidatorFix FloVer for latest HOL4 master changesSolved cheats in almost every file, only final proof leftfixpointdupsemfixpointdupsemAdd a flipped version of the IEEE connectionMerge branch 'master' of gitlab.mpi-sws.org:AVA/FloVerModernize FloVer's HOL4 filesFix for current HOL4 develop commitNew fpi_semantics using new operations on value exponent pairsInteger semantics using value exponent pairs instead of value format pairsThe furthest ffop will get with computations on MSB, version described by the reportFinite precision real equivalence with FloVerMerge branch 'fixed_point_semantics_fixes' into 'master'Defined int_semantics, more proofs, separated coercemode from fixformatresolved cheats and fixed the issue with rose_tree_indrelSeparated the monolithic file into smaller parts (also removed the nteger semantics for the moment)WIP semanticsCheckpoint 3Checkpoint 2CheckpointFixes to isJoin, isJoin3 and getValidMapFixes to morePreciseFixes to make FloVer compile with latest HOLChange Fixed-point semanticsBump .HOLCOMMIT to latest version of developFix typo in regression testing scriptBump HOLCOMMITMerge with masterDisable coq regression testsDisable Coq CI buildsMake dockerfile build the correct HOL4 version to simplify CIMerge branch 'master' of gitlab.mpi-sws.org:AVA/FloVerMake sqrt bound way more accurateUpdate regressiontests.sh to fix typoUpdate regressiontests.sh to disable binary testsUpdate ci-hol4.sh to disable binary buildAdd very coarse way of computing Sqrt for errors and intervalsFix regression testUpdate translation filesFast-forward CakeML