aboutsummaryrefslogtreecommitdiff
path: root/Makefile
Commit message (Collapse)AuthorAge
...
* "make bench", currently just X25519-C64 (closes #185)Gravatar Andres Erbsen2017-06-18
|
* compile X25519 C code from MakefileGravatar Andres Erbsen2017-06-18
|
* Don't make curves proofs on travis (hopefully fast enough build)Gravatar Jason Gross2017-06-17
|
* Fix notation-overriden warning issuesGravatar Jason Gross2017-06-15
| | | | This change is necessary because we've added -compat 8.6.
* Add -compat 8.6 to _CoqProjectGravatar Jason Gross2017-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 filesGravatar Jason Gross2017-06-14
|
* Error if Makefile.vo_closure doesn't exist and we need itGravatar Jason Gross2017-06-14
|
* Handle multiple lite-unmade-vofilesGravatar Jason Gross2017-06-12
|
* Fix lite target (typo in makefile fn call)Gravatar Jason Gross2017-06-12
|
* Better support for coq_makefile2 with fewer warningsGravatar Jason Gross2017-06-12
|
* Don't print directory when entering coqprime folderGravatar Jason Gross2017-06-11
|
* Remove Karatsuba from the lite targetGravatar Jason Gross2017-06-09
| | | | It was pretty slow.
* Compatibility with coq_makefile2Gravatar Jason Gross2017-06-01
| | | | Work harder to overwrite OTHERFLAGS if there's nothing there
* Add only-heavy targetGravatar Jason Gross2017-05-18
|
* specialize squaring earlierGravatar Andres Erbsen2017-05-14
|
* s/appcontext/context/Gravatar Jason Gross2017-05-11
| | | | They mean the same thing since 8.5, and appcontext is deprecated.
* Track .dir-locals.el rather than generating itGravatar Jason Gross2017-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 benchmarksGravatar Andres Erbsen2017-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 fixesGravatar Jason Gross2017-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 printreversedepsGravatar Jason Gross2017-04-09
|
* Add printreversedepsGravatar Jason Gross2017-04-09
|
* Display un-interped C codeGravatar Jason Gross2017-04-07
|
* Add Display files and targetsGravatar Jason Gross2017-04-07
|
* Ladderstep isn't *that* heavyGravatar Jason Gross2017-04-07
|
* Add IntegrationTestLadderstep.vGravatar Jason Gross2017-04-07
|
* Don't duplicate entries when updating _CoqProjectGravatar Jason Gross2017-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 invocationGravatar Jason Gross2017-04-06
| | | | | We don't need that part of the `sed` command anymore, now that we no longer support 8.4.
* Add note to makefileGravatar Jason Gross2017-04-03
|
* Add printdeps target to print recursive dependencies of a fileGravatar Jason Gross2017-04-03
|
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
|
* Remove everything after the individual reified opsGravatar Jason Gross2017-04-03
| | | | | This includes extraction and associated targets. I've left the .hs files lying around, currently unused.
* Remove coqprime-8.4Gravatar Jason Gross2017-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.
* Remove all the .v files in SpecificGenGravatar Jason Gross2017-04-02
| | | | This gets most of the way to 10 in #14.
* Add a "lite" targetGravatar Jason Gross2017-03-15
| | | | | | | This builds everything in the default target except WeierstrassCurveTheorems.vo, which, I believe, is the slowest file. This closes #129.
* Remove display .vo from default targetGravatar Jason Gross2017-03-06
|
* JavaDisplay depends on JavaNotations, not CNotationsGravatar Jason Gross2017-03-06
|
* Add rudimentary Java and C notation files, displayGravatar Jason Gross2017-02-15
|
* Don't remake .v.d. files in clean-coqprimeGravatar Jason Gross2017-01-22
|
* Update list of .PHONY targetsGravatar Jason Gross2017-01-09
|
* Better version of path separator usageGravatar Jason Gross2017-01-07
| | | | Thanks, @cpitclaudel !
* Kludge to get a Windows-valid .dir-locals.elGravatar Jason Gross2017-01-07
| | | | | Pass in PATHSEP=";" to `make .dir-locals.el`. Hopefully I'll find a better way soon.
* Replace $(shell pwd) with ${CURDIR}Gravatar Jason Gross2017-01-05
| | | | | | On Cygwin, `$(shell pwd)` gives a Linux path (`/cygdrive/...`), which is wrong. We now use `${CURDIR}`, as per http://stackoverflow.com/a/3679235.
* Add medium-specific-genGravatar Jason Gross2016-11-15
|
* Add a small-specific-gen targetGravatar Jason Gross2016-11-15
|
* extraction: inline field operations into group operationsGravatar Andres Erbsen2016-11-14
|
* Proper_sqrtGravatar Andres Erbsen2016-11-13
|
* Separate out SpecificGen from default targetGravatar Jason Gross2016-11-13
|
* extraction less slowGravatar Andres Erbsen2016-11-11
|
* implement X25519Gravatar Andres Erbsen2016-11-06
|
* fix extraction directives -- tested enc((l+1)B)=enc(B)Gravatar Andres Erbsen2016-11-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 09:58:20 +0000