Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add note to makefile | Jason Gross | 2017-04-03 |
| | |||
* | Add printdeps target to print recursive dependencies of a file | Jason Gross | 2017-04-03 |
| | |||
* | Remove old reflective pipeline, making way the new | Jason Gross | 2017-04-03 |
| | |||
* | Remove everything after the individual reified ops | Jason Gross | 2017-04-03 |
| | | | | | This includes extraction and associated targets. I've left the .hs files lying around, currently unused. | ||
* | Remove coqprime-8.4 | Jason Gross | 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. | ||
* | Remove all the .v files in SpecificGen | Jason Gross | 2017-04-02 |
| | | | | This gets most of the way to 10 in #14. | ||
* | Add a "lite" target | Jason Gross | 2017-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 target | Jason Gross | 2017-03-06 |
| | |||
* | JavaDisplay depends on JavaNotations, not CNotations | Jason Gross | 2017-03-06 |
| | |||
* | Add rudimentary Java and C notation files, display | Jason Gross | 2017-02-15 |
| | |||
* | Don't remake .v.d. files in clean-coqprime | Jason Gross | 2017-01-22 |
| | |||
* | Update list of .PHONY targets | Jason Gross | 2017-01-09 |
| | |||
* | Better version of path separator usage | Jason Gross | 2017-01-07 |
| | | | | Thanks, @cpitclaudel ! | ||
* | Kludge to get a Windows-valid .dir-locals.el | Jason Gross | 2017-01-07 |
| | | | | | Pass in PATHSEP=";" to `make .dir-locals.el`. Hopefully I'll find a better way soon. | ||
* | Replace $(shell pwd) with ${CURDIR} | Jason Gross | 2017-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-gen | Jason Gross | 2016-11-15 |
| | |||
* | Add a small-specific-gen target | Jason Gross | 2016-11-15 |
| | |||
* | extraction: inline field operations into group operations | Andres Erbsen | 2016-11-14 |
| | |||
* | Proper_sqrt | Andres Erbsen | 2016-11-13 |
| | |||
* | Separate out SpecificGen from default target | Jason Gross | 2016-11-13 |
| | |||
* | extraction less slow | Andres Erbsen | 2016-11-11 |
| | |||
* | implement X25519 | Andres Erbsen | 2016-11-06 |
| | |||
* | fix extraction directives -- tested enc((l+1)B)=enc(B) | Andres Erbsen | 2016-11-03 |
| | |||
* | separate Ed25519Extraction.v, add extraction to Makefile | Andres Erbsen | 2016-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-ltac | Jason Gross | 2016-09-20 |
| | |||
* | If COQPATH is not set, set it by default (#38) | Jason Gross | 2016-07-25 |
| | | | This allows most users to not need to type COQPATH=... on make. | ||
* | In >= 8.6, disable some very noisy warnings | Jason Gross | 2016-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 target | Jason Gross | 2016-07-21 |
| | |||
* | Fix clean target | Jason Gross | 2016-07-21 |
| | | | | This is the problem with copy-paste solutions. (Thanks @jadephilipoom) | ||
* | Add support for TIMED=1 in Coq 8.4 | Jason Gross | 2016-07-20 |
| | | | | This should fix #34 | ||
* | Don't depend on the submodule; copy-paste instead | Jason Gross | 2016-07-20 |
| | |||
* | Add a separate non-specific target | Jason Gross | 2016-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.el | Jason Gross | 2016-07-20 |
| | | | | | | This fixes #31 Thanks @cpitclaudel! | ||
* | Clean up the makefile a bit | Jason Gross | 2016-07-06 |
| | |||
* | Fix coqprime clean, install targets, add cleanall | Jason Gross | 2016-07-06 |
| | |||
* | Flip the sense of the conditional in the makefile | Jason Gross | 2016-06-22 |
| | | | | This way, we treat trunk as 8.5. | ||
* | Make Coq 8.5 the default target for Fiat-Crypto | Jason Gross | 2016-06-22 |
| | | | | Instructions for 8.4 build in the README | ||
* | Makefile: build on Arch Linux once again | Andres Erbsen | 2016-06-20 |
| | |||
* | Be a bit more quiet on make unless VERBOSE=1 is passed | Jason Gross | 2016-06-16 |
| | |||
* | 8.5 fixes | Jason Gross | 2016-06-10 |
| | |||
* | Add coqprime that works with 8.5, bundle bedrock | Jason Gross | 2016-06-10 |
| | | | | | | This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build. | ||
* | Makefile: single-quotes for shell globbing | Andres Erbsen | 2016-02-28 |
| | |||
* | Factor out some bedrock dependencies into WordUtil | Jason Gross | 2016-02-25 |
| | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | Update build process to use COQPATH & _CoqProject | Jason Gross | 2016-02-05 |
| | | | | | | | | Removed all of the files not built by default; they can be resurrected from git history. _CoqProject is the standard way to list the files in a project and to give information to coq_makefile. COQPATH is the standard way to make use of not-yet-installed libraries that are not part of your project (i.e., you don't want to remove them when you `make clean`, etc.). | ||
* | recursive-build coqprime | Rob Sloan | 2016-01-28 |
| | |||
* | recursive-build coqprime | Rob Sloan | 2016-01-28 |
| | |||
* | Import coqprime; use it to prove Euler's criterion. | Jade Philipoom | 2016-01-20 |
| | |||
* | remove fiat dependency | Andres Erbsen | 2016-01-16 |
| | |||
* | simple refactor of makefile; comments | varomodt | 2016-01-09 |
| | |||
* | fix the makefile to not rebuild + module renaming | Robert Sloan | 2015-10-22 |
| |