Skip to content

Fix NTT test lint violations#7

Merged
doran2728 merged 1 commit intomasterfrom
linter-fixes
Mar 21, 2026
Merged

Fix NTT test lint violations#7
doran2728 merged 1 commit intomasterfrom
linter-fixes

Conversation

@erdkocak
Copy link
Owner

This PR fixes style-linter failures in the univariate NTT files and tests.

Changes

  • wrap long lines in the NTT sources and benchmark
  • remove banned native_decide usage
  • convert NTT regression checks to #guard-based executable tests

@doran2728
Copy link
Collaborator

Good job, LGTM.

@doran2728 doran2728 merged commit 51db7dd into master Mar 21, 2026
3 of 5 checks passed
@doran2728 doran2728 deleted the linter-fixes branch March 21, 2026 19:16
@github-actions
Copy link

Build Timing Report

  • Commit: f971ccb
  • Message: Merge a56b9a6 into e43b06a
  • Ref: linter-fixes
  • Comparison baseline: e43b06a from merge-base on master.
  • Measured on ubuntu-latest with /usr/bin/time -p.
  • Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.
Measurement Baseline (s) Current (s) Delta (s) Status
Clean build 256.14 263.02 +6.88 ok
Warm rebuild 1.82 1.80 -0.02 ok
Test path 22.05 23.23 +1.18 ok

Incremental Rebuild Signal

  • Warm rebuild saved 261.22s vs clean (146.12x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s) Baseline (s) Delta (s) Path
85.00 84.00 +1.00 CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean
52.00 55.00 -3.00 CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
49.00 49.00 +0.00 CompPoly/Bivariate/ToPoly.lean
29.00 28.00 +1.00 CompPoly/Univariate/Raw/Proofs.lean
28.00 31.00 -3.00 CompPoly/Fields/Binary/BF128Ghash/Impl.lean
24.00 21.00 +3.00 CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean
23.00 21.00 +2.00 CompPoly/Univariate/Lagrange.lean
21.00 23.00 -2.00 CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean
20.00 17.00 +3.00 CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean
20.00 12.00 +8.00 CompPoly/Multivariate/Unlawful.lean
17.00 18.00 -1.00 CompPoly/Univariate/Quotient/Core.lean
16.00 16.00 +0.00 CompPoly/Fields/Binary/AdditiveNTT/Domain.lean
16.00 16.00 +0.00 CompPoly/Univariate/Basic.lean
15.00 13.00 +2.00 CompPoly/Fields/Binary/Common.lean
14.00 12.00 +2.00 CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean
14.00 15.00 -1.00 CompPoly/Fields/Binary/Tower/Abstract/Core.lean
13.00 10.00 +3.00 CompPoly/Fields/Binary/Tower/TensorAlgebra.lean
11.00 9.70 +1.30 CompPoly/Fields/Binary/Tower/Abstract/Split.lean
11.00 11.00 +0.00 CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean
11.00 10.00 +1.00 CompPoly/Multivariate/MvPolyEquiv/Instances.lean

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants