Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | fix .h dependencies in makefile (closes #235) | 2017-07-05 | ||
| | ||||
* | benchmarking: correct for differences in CPU and TSC frequency | 2017-07-05 | ||
| | ||||
* | use att style assembly with icc, test it | 2017-07-04 | ||
| | ||||
* | test p256 mixed addition | 2017-07-04 | ||
| | | | | | passed after fixing some stupid typos in glue code -- no conceptual issues. | |||
* | fix mulx argument order using sed, test feadd, femul (fails due to #234) | 2017-07-03 | ||
| | ||||
* | X25519 test (passed on first try) | 2017-07-02 | ||
| | ||||
* | automate P256 integration | 2017-07-02 | ||
| | ||||
* | make bench: include all benchmarks | 2017-07-01 | ||
| | ||||
* | benchmark OpenSSL p256 C code | 2017-07-01 | ||
| | ||||
* | benchmark OpenSSL curve25519 | 2017-07-01 | ||
| | ||||
* | Add proper dependencies on .h file in Makefile | 2017-06-29 | ||
| | ||||
* | Make the same display on windows and linux | 2017-06-28 | ||
| | | | | Do this by removing windows line endings via sed | |||
* | p256 compilation and benchmarks with manual kludges | 2017-06-27 | ||
| | ||||
* | Drop the two slowest files from the lite target | 2017-06-26 | ||
| | ||||
* | add openssl nistz256 for benchmarking | 2017-06-23 | ||
| | ||||
* | Makefile: c: h | 2017-06-20 | ||
| | ||||
* | don't key benchmarks on cpu frequency | 2017-06-18 | ||
| | ||||
* | measurements.txt depends on scripts that generate it | 2017-06-18 | ||
| | ||||
* | "make bench", currently just X25519-C64 (closes #185) | 2017-06-18 | ||
| | ||||
* | compile X25519 C code from Makefile | 2017-06-18 | ||
| | ||||
* | Don't make curves proofs on travis (hopefully fast enough build) | 2017-06-17 | ||
| | ||||
* | Fix notation-overriden warning issues | 2017-06-15 | ||
| | | | | This change is necessary because we've added -compat 8.6. | |||
* | Add -compat 8.6 to _CoqProject | 2017-06-15 | ||
| | | | | | | This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet). | |||
* | Add a printlite target to display lite files | 2017-06-14 | ||
| | ||||
* | Error if Makefile.vo_closure doesn't exist and we need it | 2017-06-14 | ||
| | ||||
* | Handle multiple lite-unmade-vofiles | 2017-06-12 | ||
| | ||||
* | Fix lite target (typo in makefile fn call) | 2017-06-12 | ||
| | ||||
* | Better support for coq_makefile2 with fewer warnings | 2017-06-12 | ||
| | ||||
* | Don't print directory when entering coqprime folder | 2017-06-11 | ||
| | ||||
* | Remove Karatsuba from the lite target | 2017-06-09 | ||
| | | | | It was pretty slow. | |||
* | Compatibility with coq_makefile2 | 2017-06-01 | ||
| | | | | Work harder to overwrite OTHERFLAGS if there's nothing there | |||
* | Add only-heavy target | 2017-05-18 | ||
| | ||||
* | specialize squaring earlier | 2017-05-14 | ||
| | ||||
* | s/appcontext/context/ | 2017-05-11 | ||
| | | | | They mean the same thing since 8.5, and appcontext is deprecated. | |||
* | Track .dir-locals.el rather than generating it | 2017-04-24 | ||
| | | | | | Since we're only using one version of coqprime, we no longer need to generate .dir-locals.el | |||
* | X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarks | 2017-04-13 | ||
| | | | | | | | | | | | | | | | | 21% slower than donna 36% slower than assembly with saturated limbs. cycles impl compiler 593072 crypto_scalarmult/curve25519/amd64-64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer 636660 crypto_scalarmult/curve25519/amd64-51 gcc_-funroll-loops_-fno-schedule-insns_-O2_-fomit-frame-pointer 660220 crypto_scalarmult/curve25519/donna_c64 gcc_-m64_-march=native_-mtune=native_-O3_-fomit-frame-pointer 804684 crypto_scalarmult/curve25519/fiat_c64 clang_-march=native_-O3_-fomit-frame-pointer_-fwrapv_-Qunused-arguments 815716 crypto_scalarmult/curve25519/fiat_c64 gcc_-m64_-march=core-avx2_-O3_-fomit-frame-pointer Setup: Broadwell i7-5600U 2.60GHz in an X1C3. no HT, no TB, wall power. Journalctl did not record any thermal throttling, idk if trustworthy. Cc: @achlipala @JasonGross @jadephilipoom | |||
* | Makefile fixes | 2017-04-09 | ||
| | | | | | | | Fix the lite target to remove all transitive (reverse) dependencies. Don't run `coqtop` to get the version unless we're actually going to use it to build things | |||
* | Fix printreversedeps | 2017-04-09 | ||
| | ||||
* | Add printreversedeps | 2017-04-09 | ||
| | ||||
* | Display un-interped C code | 2017-04-07 | ||
| | ||||
* | Add Display files and targets | 2017-04-07 | ||
| | ||||
* | Ladderstep isn't *that* heavy | 2017-04-07 | ||
| | ||||
* | Add IntegrationTestLadderstep.v | 2017-04-07 | ||
| | ||||
* | Don't duplicate entries when updating _CoqProject | 2017-04-07 | ||
| | | | | This can happen if you're in the middle of resolving a merge conflict (git ls-files will list some files twice). | |||
* | Clean up coq_makefile invocation | 2017-04-06 | ||
| | | | | | We don't need that part of the `sed` command anymore, now that we no longer support 8.4. | |||
* | Add note to makefile | 2017-04-03 | ||
| | ||||
* | Add printdeps target to print recursive dependencies of a file | 2017-04-03 | ||
| | ||||
* | Remove old reflective pipeline, making way the new | 2017-04-03 | ||
| | ||||
* | Remove everything after the individual reified ops | 2017-04-03 | ||
| | | | | | This includes extraction and associated targets. I've left the .hs files lying around, currently unused. | |||
* | Remove coqprime-8.4 | 2017-04-02 | ||
| | | | | | | | We're using tactics in terms in some places, and so have no hope of compiling with Coq 8.4. We no longer pretend to support it. We can probably also remove some other compatibility things, if we want. |