Skip to content

Issues: hacspec/hax

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

209 Open 391 Closed
209 Open 391 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

fold_range type mismatch f* F* backend
#1214 opened Dec 31, 2024 by franziskuskiefer
2
Could not solve typeclass constraint f* F* backend
#1213 opened Dec 28, 2024 by franziskuskiefer
Run F* lax-checking on tests f* F* backend tests Issue related to tests, CI or examples
#1211 opened Dec 24, 2024 by maximebuyse
Implement return / break / continue loop fold operators for f* f* F* backend libcore
#1204 opened Dec 19, 2024 by maximebuyse
@maximebuyse
2
Trait method calls don't get renamed properly inside bundles
#1203 opened Dec 19, 2024 by maximebuyse
No rewriting of $ names in fstar! macro with bundling annotations
#1196 opened Dec 18, 2024 by maximebuyse
1
Needs Design: Allow &mut and raw pointer returning functions in interfaces needs-design We need to write a proper design for this issue.
#1195 opened Dec 18, 2024 by karthikbhargavan
F* cannot prove decidable equality with Hashmaps f* F* backend libcore
#1194 opened Dec 17, 2024 by maximebuyse
1
Bundle bug with recursion
#1186 opened Dec 12, 2024 by W95Psp
Generate axioms for items with Erased attribute in the coq backend backend Issue in one of the backends (i.e. F*, Coq, EC...) coq Coq backend
#1185 opened Dec 12, 2024 by maximebuyse
Allow all hax-lib attributes on impl elements lib Lib-related issue (e.g. annotations lib)
#1183 opened Dec 11, 2024 by karthikbhargavan
Macro: requires and ensures should produce doc strings
#1178 opened Dec 10, 2024 by W95Psp
Crash with hax_lib::fstar::before in recursive bundle bug Something isn't working engine Issue in the engine
#1177 opened Dec 10, 2024 by maximebuyse
1
@maximebuyse
1
Fatal error in side_effect_utils.ml
#1175 opened Dec 9, 2024 by franziskuskiefer
1
[Meta] Iterator support keep-open meta
#1173 opened Dec 9, 2024 by franziskuskiefer
1
F* extraction hangs
#1172 opened Dec 9, 2024 by franziskuskiefer
@W95Psp
2
continue not working in while loop
#1171 opened Dec 7, 2024 by franziskuskiefer
3
Constructor prefixed with t_ in rec bundle bug Something isn't working engine Issue in the engine
#1169 opened Dec 3, 2024 by maximebuyse
Fstar core modelling of IntoIterator trait fails on some generated code using it bug Something isn't working f* F* backend libcore
#1168 opened Dec 3, 2024 by maximebuyse
1
Ghost variables for proofs enhancement New feature or request lib Lib-related issue (e.g. annotations lib)
#1167 opened Dec 3, 2024 by karthikbhargavan
from method provided by core::convert::From is not extracted to the same name if it passed as a closure bug Something isn't working engine Issue in the engine f* F* backend
#1165 opened Dec 3, 2024 by maximebuyse
2
Book: architecture: add diagram documentation Improvements or additions to documentation
#1164 opened Dec 3, 2024 by W95Psp
Engine: global names: change the representation from krate * path to path * path * item
#1163 opened Dec 3, 2024 by W95Psp
@W95Psp
1
Engine: name clash for items within trait methods
#1161 opened Dec 3, 2024 by W95Psp
Engine: F*: stop relying on F* builtin equality
#1160 opened Dec 3, 2024 by W95Psp
ProTip! Exclude everything labeled bug with -label:bug.