Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Don't remake .v.d. files in clean-coqprime | 2017-01-22 | |
| | |||
* | Update list of .PHONY targets | 2017-01-09 | |
| | |||
* | Better version of path separator usage | 2017-01-07 | |
| | | | | Thanks, @cpitclaudel ! | ||
* | Kludge to get a Windows-valid .dir-locals.el | 2017-01-07 | |
| | | | | | Pass in PATHSEP=";" to `make .dir-locals.el`. Hopefully I'll find a better way soon. | ||
* | Replace $(shell pwd) with ${CURDIR} | 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 | 2016-11-15 | |
| | |||
* | Add a small-specific-gen target | 2016-11-15 | |
| | |||
* | extraction: inline field operations into group operations | 2016-11-14 | |
| | |||
* | Proper_sqrt | 2016-11-13 | |
| | |||
* | Separate out SpecificGen from default target | 2016-11-13 | |
| | |||
* | extraction less slow | 2016-11-11 | |
| | |||
* | implement X25519 | 2016-11-06 | |
| | |||
* | fix extraction directives -- tested enc((l+1)B)=enc(B) | 2016-11-03 | |
| | |||
* | separate Ed25519Extraction.v, add extraction to Makefile | 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 | 2016-09-20 | |
| | |||
* | If COQPATH is not set, set it by default (#38) | 2016-07-25 | |
| | | | This allows most users to not need to type COQPATH=... on make. | ||
* | In >= 8.6, disable some very noisy warnings | 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 | 2016-07-21 | |
| | |||
* | Fix clean target | 2016-07-21 | |
| | | | | This is the problem with copy-paste solutions. (Thanks @jadephilipoom) | ||
* | Add support for TIMED=1 in Coq 8.4 | 2016-07-20 | |
| | | | | This should fix #34 | ||
* | Don't depend on the submodule; copy-paste instead | 2016-07-20 | |
| | |||
* | Add a separate non-specific target | 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 | 2016-07-20 | |
| | | | | | | This fixes #31 Thanks @cpitclaudel! | ||
* | Clean up the makefile a bit | 2016-07-06 | |
| | |||
* | Fix coqprime clean, install targets, add cleanall | 2016-07-06 | |
| | |||
* | Flip the sense of the conditional in the makefile | 2016-06-22 | |
| | | | | This way, we treat trunk as 8.5. | ||
* | Make Coq 8.5 the default target for Fiat-Crypto | 2016-06-22 | |
| | | | | Instructions for 8.4 build in the README | ||
* | Makefile: build on Arch Linux once again | 2016-06-20 | |
| | |||
* | Be a bit more quiet on make unless VERBOSE=1 is passed | 2016-06-16 | |
| | |||
* | 8.5 fixes | 2016-06-10 | |
| | |||
* | Add coqprime that works with 8.5, bundle bedrock | 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 | 2016-02-28 | |
| | |||
* | Factor out some bedrock dependencies into WordUtil | 2016-02-25 | |
| | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | Update build process to use COQPATH & _CoqProject | 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 | 2016-01-28 | |
| | |||
* | recursive-build coqprime | 2016-01-28 | |
| | |||
* | Import coqprime; use it to prove Euler's criterion. | 2016-01-20 | |
| | |||
* | remove fiat dependency | 2016-01-16 | |
| | |||
* | simple refactor of makefile; comments | 2016-01-09 | |
| | |||
* | fix the makefile to not rebuild + module renaming | 2015-10-22 | |
| | |||
* | pull changes from desktop | 2015-10-19 | |
| | |||
* | redo module structure + init curve25519 | 2015-09-16 | |
| | |||
* | Basic Galois Field Theory Modules | 2015-09-16 | |
| | |||
* | init our centralized repo | 2015-09-10 | |