v1.2.0

Added

• Added two new fields in extract_theorems to be consistent with extract_decls (see below):
  • kind: always theorem for extract_theorems.
  • declaration_messages: same content as theorem_messages. theorem_messages is now deprecated and will be removed in a future update.
• Added extract_decls, an upgraded version of extract_theorems that extracts all declaration kinds.
  • New kind field in each document. Possible values: theorem, def, abbrev, axiom, opaque, structure, class, class inductive, inductive, instance, example, unknown
  • Note: Not all fields are meaningful for all declaration kinds (e.g., proof_length/tactic_counts only apply to theorems/lemmas with tactic proofs.)
  • This tool should be used instead of extract_theorems as it is a strict superset of functionality. extract_theorems will be deprecated in a future update.

Fixed

• Added "Last Used" and "Requests (24h)" columns to the API key console page for better visibility into API key usage.

v1.1.1

Changed

• [!] We are turning on the autoImplicit and turning off the pp.unicode.fun Lean options. AXLE will now automatically insert implicit variables when they are missing. This is a significant behavioral change, check your code! These settings are consistent with Lean's default. The previous options were remnants from internal use preferences.
• [!] We have renamed mathlib_linter to mathlib_options, which now sets linter.mathlibStandardSet to true, autoImplicit to false, relaxedAutoImplicit to false, and pp.unicode.fun to true. Use this toggle to enable the stricter defaults that Mathlib uses by convention.

Added

• Added Lean 4.29.0 support.
• Added support for glob patterns in the permitted_sorries field for verify_proof. See the verify_proof documentation page under the permitted_sorries field for example use cases.

Fixed

• Fixed a bug causing timeouts to be capped at 10 minutes. All requests now max out at 15 minutes (with documentation updated correspondingly).

v1.1.0

Changed

• [!] Removed document_messages from the response of extract_theorems — to replicate old behavior, run the content field of the resulting documents through the check tool. This change significantly improves the speed of extract_theorems.
• [!] includeEndPos has been turned on for Lean messages. This changes the format from:
  -:4:38: error: Function expected at...
  to (when endPos is available):
  -:4:38-4:43: error: Function expected at...
  This change affects all tools with Lean messages.
• Significantly reworked the Lean executor pool backend.
  • Latency has been decreased by 50% in most cases. For longer requests, the new executors can be more than 5 times faster!
  • Previously, the first request to each environment required a ~10s warmup. This is no longer the case, and so requests will be more faithful to their Lean timeout limits (not including queueing / waiting for available slots).
  • Eliminates a security risk involving persistent Lean workers.
• Improved the Lean worker warm-up pipeline. Worker scale-up is also more aggressive than before. In the worst case, when all workers are completely occupied / offline, users should expect no more than a 2-3 minute delay before more worker capacity spins up.

Fixed

• Removed redundant parsing resulting in occasional speedups in repair_proofs, normalize, etc. when content does not change.
• Pruned missing executors from the gateway registry. Fixes a bug with autoscaling improperly triggering.

Internal

• Lean workers are now ephemeral and live just long enough to serve a single request. Speed is maintained by using a warmed-up parent process that forks child workers. Workers are now properly isolated from each other security-wise, but shared COW environments mean that memory usage is significantly reduced, opening up the opportunity for further optimizations without memory as a bottleneck. The parent warm-up process also invokes new opportunities to pre-load heavy data structures, such as those in suggestion-engine-4.28.0.
• Removed /dev/shm, increased the number of procs to 32/executor, and changed the executor instance type to c8a.8xlarge, resulting in a more than 2x latency speedup.
• Improved the warm-up pipeline to warm-up all environments at the start, eliminating warm-up times per request.
• Fixed a disk I/O throughput configuration parameter omission causing warm-up to be extraordinarily slow.
• Introduced an executor ASG warm pool with instances stored in Stopped mode. Hibernated mode was explored but did not work correctly.
• Introduced a DB archiver which regularly polls the request database and archives old requests to S3.
• Added a CloudWatch alarm to remind admins to update the Tailscale API key every 3 months.
• Updated axiomlib-4.27.0 to axiomlib-4.28.0.
• Created an executor launch lifecycle hook to prevent them from being registered as InService before they are ready to serve requests.
• Allow executors to gracefully shut down, draining all requests before terminating.
• Lowered gateway cache size to prevent gateway crashes from running out of memory.
• Fixed a bug where Lean worker error output was not being drained, causing it to deadlock.

v1.0.2

Added

• Added explicit okay return value to repair_proofs

Changed

• Improved error messages for unknown options in simplify_theorems, repair_proofs, normalize
• Improved error messages for ignore_imports error (with links to relevant docs)
• Improved the efficiency of merge, bringing down the time spent on large requests by 20-30%.

v1.0.1

Added

• Added Changelog and Troubleshooting to the documentation pages.

Fixed

• Increased request limits and fixed a typo in the documentation. Users with an API key are now limited to 20 active requests, and anonymous users are limited to 10 active requests.
• Increased maximum timeout to 15 minutes (from 5 minutes).
• Environments are now sorted by prefix (alphabetically) and then by version number (more recent versions first)
• Fixed a bug with disprove failing to recognize implicit local variables. This bug was found by Bulhwi Cha on Lean Zulip.

v1.0.0

Released

• Initial release of AXLE Python client
• Async client (AxleClient) with all 13 API tools:
  • verify_proof - Verify proofs against formal statements
  • check - Check Lean code for errors
  • extract_theorems - Extract theorems with dependencies
  • rename - Rename declarations
  • theorem2lemma - Convert theorem/lemma keywords
  • theorem2sorry - Replace proofs with sorry
  • merge - Combine multiple Lean files
  • simplify_theorems - Simplify proofs
  • repair_proofs - Repair broken proofs
  • have2lemma - Extract have statements to lemmas
  • have2sorry - Replace have statements with sorry
  • disprove - Attempt to disprove theorems
  • normalize - Standardize formatting
• CLI tool with commands for all tools
• Helper functions for string manipulation
• Configuration via environment variables
• Type hints and PEP 561 compliance
• Comprehensive documentation