Skip to content

Issues: AeneasVerif/aeneas

Beta
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

89 Open 92 Closed
89 Open 92 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Unexpected simp_ifs behaviour
#516 opened May 6, 2025 by ayhon
Incorrect extraction on loop with copy
#500 opened Apr 13, 2025 by ayhon
3
eval_global fails on usize and isize expressions.
#492 opened Apr 9, 2025 by ayhon
1
simp_lists not going inside forallE
#487 opened Apr 7, 2025 by ayhon
Update PureTypeCheck and fix the type-checking errors
#486 opened Apr 7, 2025 by sonmarcho
progres*? shows Aesop's add this message.
#476 opened Mar 27, 2025 by ayhon
Sometimes invalid identifiers are used as names in definitions
#475 opened Mar 27, 2025 by ayhon
Array is unable to handle arrays of length > 161
#474 opened Mar 27, 2025 by ayhon
7
Functions using definitions extracted as axioms are not marked noncomputable.
#473 opened Mar 27, 2025 by ayhon
Support the vec! macro
#469 opened Mar 25, 2025 by ayhon
3
Internal error when iterating on a Vec of slices
#464 opened Mar 24, 2025 by ayhon
1
Detect looping equalities in scalar_tac
#448 opened Mar 6, 2025 by sonmarcho
Reorganize the Lean backend to improve the build time
#447 opened Mar 6, 2025 by sonmarcho
Correctly namespace default trait methods
#438 opened Feb 12, 2025 by Nadrieril
@sonmarcho
Improve the saturate tactic for scalar_tac
#433 opened Feb 4, 2025 by sonmarcho
Use the definitions from the standard library of Lean for the scalars
#427 opened Feb 1, 2025 by sonmarcho
this fib code should work
#425 opened Jan 27, 2025 by bizid777
2
The use of opaque functions without --split-files generates files which don't typecheck in Lean
#420 opened Jan 17, 2025 by sonmarcho
The filtering of parameters for builtin definitions happens after the computation of the implicit parameters
#415 opened Jan 14, 2025 by sonmarcho
2
PrePasses.remove_loop_breaks is very slow
#401 opened Dec 18, 2024 by sonmarcho
Unexpected error
#400 opened Dec 18, 2024 by sonmarcho
4
Improve error message about printing macros (println!/dbg!)
#398 opened Dec 16, 2024 by Cemoixerestre
Document using Charon attributes for Aeneas extraction
#396 opened Dec 12, 2024 by R1kM
Improve error message about bottoms
#392 opened Dec 10, 2024 by shaoweilin
1
Improve the extraction of code manipulating arrays/slices
#381 opened Dec 3, 2024 by sonmarcho
2
ProTip! Updated in the last three days: updated:>2025-05-27.