| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
|
|
|
|
|
|
|
|
|
|
| |
This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6.
Revert "Move weqb_hetero to Bedrock.Word"
This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763.
We probably shouldn't modify Bedrock.Word
|
| |
|
|
|
|
| |
This reverts commit a66ba3e5202adcc436c3a1fcf6433261e7bdd158.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change
--------------------------------------------------------------------------------------
3m22.43s | Total | 3m22.13s || +0m00.30s
--------------------------------------------------------------------------------------
0m34.51s | Spec/Ed25519 | 0m34.56s || -0m00.05s
0m28.83s | Experiments/Ed25519 | 0m28.60s || +0m00.22s
0m17.28s | EdDSARepChange | 0m17.25s || +0m00.03s
0m08.66s | [require-in-module,deprecated]
src/Assembly/GF25519 | 0m08.66s || +0m00.00s
0m08.46s | Encoding/PointEncoding | 0m08.47s || -0m00.00s
0m08.35s | Specific/GF25519BoundedCommonWord | 0m08.44s || -0m00.08s
0m07.74s | Specific/GF25519Reflective | 0m07.69s || +0m00.04s
0m07.59s | Specific/GF25519Reflective/Reified/Mul | 0m07.65s || -0m00.06s
0m07.35s | Specific/GF25519BoundedCommon | 0m07.39s || -0m00.04s
0m06.88s | Specific/GF25519Reflective/Reified/Freeze | 0m06.86s || +0m00.01s
0m05.80s | Bedrock/Word | 0m05.74s || +0m00.05s
0m05.43s | Specific/SC25519 | 0m05.32s || +0m00.10s
0m04.76s | Reflection/Z/Interpretations | 0m04.65s || +0m00.10s
0m04.27s | Encoding/PointEncodingPre | 0m04.31s || -0m00.04s
0m03.72s | Assembly/GF25519BoundedInstantiation | 0m03.68s || +0m00.04s
0m03.21s | Specific/GF25519Reflective/Reified/CarrySub | 0m03.34s || -0m00.12s
0m02.91s | Specific/GF25519Reflective/Reified/CarryOpp | 0m02.86s || +0m00.05s
0m02.84s | Specific/GF25519Reflective/Reified/CarryAdd | 0m02.87s || -0m00.03s
0m02.70s | Assembly/State | 0m02.67s || +0m00.03s
0m02.00s | Specific/GF25519Reflective/Reified/Unpack | 0m01.96s || +0m00.04s
0m01.97s | Specific/GF25519Reflective/Reified/Sub | 0m01.95s || +0m00.02s
0m01.95s | Specific/GF25519Reflective/Reified/Pack | 0m02.03s || -0m00.07s
0m01.81s | Assembly/Evaluables | 0m01.88s || -0m00.06s
0m01.78s | Specific/GF25519Bounded | 0m01.77s || +0m00.01s
0m01.71s | Specific/GF25519Reflective/Reified/Opp | 0m01.68s || +0m00.03s
0m01.66s | Specific/GF25519Reflective/Reified/Add | 0m01.66s || +0m00.00s
0m01.52s | Assembly/Compile | 0m01.48s || +0m00.04s
0m01.49s | Specific/GF25519Reflective/Reified/GeModulus | 0m01.48s || +0m00.01s
0m01.44s | Assembly/WordizeUtil | 0m01.51s || -0m00.07s
0m01.33s | Assembly/Bounds | 0m01.34s || -0m00.01s
0m01.22s | Assembly/Conversions | 0m01.23s || -0m00.01s
0m01.05s | Util/WordUtil | 0m01.03s || +0m00.02s
0m00.94s | Assembly/LL | 0m00.94s || +0m00.00s
0m00.94s | Assembly/Pipeline | 0m00.90s || +0m00.03s
0m00.87s | Assembly/HL | 0m00.89s || -0m00.02s
0m00.81s | Assembly/PhoasCommon | 0m00.77s || +0m00.04s
0m00.79s | Assembly/QhasmEvalCommon | 0m00.83s || -0m00.03s
0m00.75s | Specific/GF25519Reflective/Reified | 0m00.80s || -0m00.05s
0m00.72s | Specific/GF25519Reflective/Common | 0m00.71s || +0m00.01s
0m00.70s | Encoding/ModularWordEncodingTheorems | 0m00.65s || +0m00.04s
0m00.66s | Spec/EdDSA | 0m00.66s || +0m00.00s
0m00.61s | Spec/ModularWordEncoding | 0m00.58s || +0m00.03s
0m00.61s | Encoding/ModularWordEncodingPre | 0m00.67s || -0m00.06s
0m00.51s | Assembly/Qhasm | 0m00.51s || +0m00.00s
0m00.48s | Assembly/StringConversion | 0m00.50s || -0m00.02s
0m00.47s | Assembly/QhasmUtil | 0m00.40s || +0m00.06s
0m00.36s | Assembly/QhasmCommon | 0m00.31s || +0m00.04s
|
| |
|
| |
|
| |
|
|
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.
|