aboutsummaryrefslogtreecommitdiff
path: root/Makefile
Commit message (Collapse)AuthorAge
* 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
|
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
| | | | | @JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment
* Allow passing PROFILE=1 to make for -profile-ltacGravatar Jason Gross2016-09-20
|
* If COQPATH is not set, set it by default (#38)Gravatar Jason Gross2016-07-25
| | | This allows most users to not need to type COQPATH=... on make.
* In >= 8.6, disable some very noisy warningsGravatar Jason Gross2016-07-25
| | | | | | | | | Since we're building for both 8.4 and 8.5, we don't want to see warnings about appcontext being deprecated. Many of the notation-overridden warnings come from standard library imports (see [bug #4962](https://coq.inria.fr/bugs/show_bug.cgi?id=4962)) so it's not clear that there's anything we can do about them.
* Faster update-_CoqProject targetGravatar Jason Gross2016-07-21
|
* Fix clean targetGravatar Jason Gross2016-07-21
| | | | This is the problem with copy-paste solutions. (Thanks @jadephilipoom)
* Add support for TIMED=1 in Coq 8.4Gravatar Jason Gross2016-07-20
| | | | This should fix #34
* Don't depend on the submodule; copy-paste insteadGravatar Jason Gross2016-07-20
|
* Add a separate non-specific targetGravatar Jason Gross2016-07-20
| | | | | | | | This should fix #27. We depend on some files in the etc/coq-scripts submodule. Note that you need to either run `make cleanall -k` or `rm -f Makefile.coq` after pulling this to build the development.
* Add target for .dir-locals.elGravatar Jason Gross2016-07-20
| | | | | | This fixes #31 Thanks @cpitclaudel!
* Clean up the makefile a bitGravatar Jason Gross2016-07-06
|
* Fix coqprime clean, install targets, add cleanallGravatar Jason Gross2016-07-06
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 00:44:44 +0000