Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / FStarLang/FStar issues and pull requests

#3465 - Sealed: mark seal/unseal as coercions

Pull Request - State: open - Opened by mtzguido 2 months ago - 3 comments

#3464 - Assumed function should block tactic

Issue - State: open - Opened by mtzguido 2 months ago

#3462 - --include of a non existent directory should work

Issue - State: closed - Opened by briangmilnes 2 months ago

#3461 - Nits

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3460 - Add normalization step for tactics.

Pull Request - State: closed - Opened by gebner 2 months ago - 3 comments

#3459 - Make seal/unseal coercions

Issue - State: open - Opened by mtzguido 2 months ago

#3457 - dune tweaks: no cmt and no bytecode

Pull Request - State: closed - Opened by mtzguido 2 months ago - 1 comment

#3456 - Multiple --cache_dir s for multi-directory compilations

Issue - State: open - Opened by briangmilnes 2 months ago - 3 comments

#3455 - Extraction.Krml: properly detect mem type, it does not have an argument

Pull Request - State: closed - Opened by mtzguido 2 months ago - 1 comment

#3454 - src: use fstar.include

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3453 - Improving internal error API

Pull Request - State: closed - Opened by mtzguido 2 months ago - 1 comment

#3452 - ulib: move hints to separate directory

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3451 - Misc

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3450 - Unexpected error when missing all files

Issue - State: open - Opened by briangmilnes 2 months ago - 3 comments

#3449 - fix: use more precise types for `move_requires_*`

Pull Request - State: closed - Opened by TWal 2 months ago - 2 comments

#3448 - Cannot match implicit arg using constructor

Issue - State: open - Opened by mtzguido 2 months ago - 1 comment

#3447 - Feature flag

Issue - State: open - Opened by mtzguido 2 months ago

#3446 - A fix in tactics, do not set uvar_subtyping=false so eagerly

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3444 - Advance to 2024.09.05~dev

Pull Request - State: closed - Opened by dzomo 2 months ago - 1 comment

#3443 - Ide fixes

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3442 - checkworld tweaks

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3441 - Adding Pulse bootstrapping test to check-world

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3440 - SMT context pruning

Pull Request - State: closed - Opened by nikswamy 2 months ago

#3438 - CI Tweaks

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3437 - parser: publish more symbols for Pulse

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3436 - Fixing short circuting operators when --admit

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3435 - Misc fix

Pull Request - State: closed - Opened by mtzguido 2 months ago

#3434 - Distribution size of FStar

Issue - State: open - Opened by kant2002 2 months ago - 3 comments

#3433 - actions: check-world workflow

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3432 - Parser.Dep: interpret inline_for_extraction on *any* decl, not just Vals

Pull Request - State: closed - Opened by mtzguido 3 months ago - 1 comment

#3431 - Some fixes

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3430 - feat(syntax): any terms in meta arguments

Pull Request - State: closed - Opened by W95Psp 3 months ago - 1 comment

#3429 - Please print the z3rlimit on error 19

Issue - State: closed - Opened by briangmilnes 3 months ago

#3428 - ulib: FStar.Range: allow inspecting the unsealed __range

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3427 - Fix encoding of primitive operators with refined domains

Pull Request - State: closed - Opened by nikswamy 3 months ago

#3426 - Refinement subtypes being discarded

Issue - State: open - Opened by amosr 3 months ago - 6 comments

#3425 - Refactoring printers

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3424 - Some makefile fixes

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3423 - Move away from deprecated batteries functions.

Pull Request - State: open - Opened by gebner 3 months ago

#3422 - Push CI images to ghcr.io

Pull Request - State: open - Opened by gebner 3 months ago

#3421 - Avoid wildcard expansion when making F# builds

Pull Request - State: closed - Opened by jonahbeckford 3 months ago - 6 comments

#3420 - Some rework of the options module

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3419 - Main: introduce --read_krml_file mode

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3417 - introduce tests/krml with karamel unit tests

Pull Request - State: closed - Opened by mtzguido 3 months ago - 1 comment

#3416 - Using monoids for tc guards in TcTerm

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3415 - Tc: rework attribute-tagged implicits to require defer_to

Pull Request - State: closed - Opened by mtzguido 3 months ago - 1 comment

#3414 - A bit more refactor

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3413 - Refactoring implicit instantiation

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3412 - Misc improvements in library

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3411 - Dep graph visualization

Pull Request - State: open - Opened by mtzguido 3 months ago

#3410 - Revert "UInt128: break dependency on FStar.Int.Cast"

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3409 - normalizer: a fix for a plugin returned by a function

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3408 - FStar.Char: move type into smaller FStar.Char.Type module

Pull Request - State: open - Opened by mtzguido 3 months ago - 4 comments

#3407 - Deps

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3406 - Introduce an attribute to unrefine type arguments

Pull Request - State: closed - Opened by mtzguido 3 months ago - 2 comments

#3405 - Optimizing CI

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3404 - actions/docker: reworking ci to just run `make ci-post`

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3403 - Reflection: V2: support Equality qualifier for binders

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3402 - Windows CI using DkML

Pull Request - State: open - Opened by jonahbeckford 3 months ago

#3401 - Tactics: remove canon tests from ulib/, place in new tests/

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3400 - actions: updating dependencies

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3399 - Normalizer: introduce DontUnfoldAttr, discard UnfoldTac

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3398 - FStar.fst.config.json: make sure to use *this* fstar.exe

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3397 - Bump OCaml version to 4.14

Pull Request - State: closed - Opened by gebner 3 months ago

#3396 - LowStar.Monotonic.Buffer: mark loc erasable

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3395 - Tc: improving error for mistaking fields in a record

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3394 - Fix Makefile

Pull Request - State: closed - Opened by mtzguido 3 months ago

#3382 - Use the MkProjectors tactic for all typeclasses

Pull Request - State: open - Opened by mtzguido 3 months ago - 2 comments

#3378 - Do not require parentheses for fun/assume/assert

Pull Request - State: closed - Opened by gebner 3 months ago - 8 comments

#3366 - Incorrect erasure of function types

Issue - State: open - Opened by gebner 4 months ago - 3 comments

#3345 - RFC: An fstar.include file to simplify `--include`

Pull Request - State: closed - Opened by mtzguido 4 months ago - 2 comments

#3204 - Splitting tuple types into separate modules for each

Pull Request - State: open - Opened by mtzguido 10 months ago - 2 comments

#3169 - Add `[@@no_inline_let]` annotation

Pull Request - State: open - Opened by amosr 11 months ago - 9 comments

#3144 - cannot be installed via `opam pin` in `opam` sandboxes

Issue - State: open - Opened by shonfeder 12 months ago - 1 comment

#2828 - Z3 4.8.5 fails to build on ARM macs

Issue - State: open - Opened by h0wk-b1rd13 almost 2 years ago

#2653 - Deliberately use small version number

Pull Request - State: closed - Opened by kant2002 over 2 years ago

#2420 - The following actions failed │ λ build conf-python-2-7 1.2

Issue - State: closed - Opened by Chaos-Crypto almost 3 years ago - 7 comments

#100 - by_induction_on fails for lemmas with two arguments

Issue - State: closed - Opened by ckeller almost 10 years ago - 3 comments
Labels: kind/enhancement, status/wont-fix

#99 - Nesting function slows down the type checking process

Issue - State: closed - Opened by VincentCheval almost 10 years ago - 3 comments

#98 - Using FStar interface

Issue - State: closed - Opened by VincentCheval almost 10 years ago - 5 comments
Labels: kind/enhancement

#97 - Parsing problem with forall and type declaration

Issue - State: closed - Opened by VincentCheval almost 10 years ago - 1 comment
Labels: kind/bug

#96 - Blow-up in SMT encoding

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 5 comments
Labels: kind/bug

#95 - "logic" qualifier for inductive relations

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 3 comments
Labels: kind/enhancement

#94 - Codegen to F#

Issue - State: closed - Opened by mikhail-makarov almost 10 years ago - 7 comments
Labels: kind/enhancement, component/extraction

#93 - There is no utils.fst mentioned in INSTALL.md

Issue - State: closed - Opened by mikhail-makarov almost 10 years ago

#92 - Problem when defining and using type representing functions

Issue - State: closed - Opened by VincentCheval almost 10 years ago - 2 comments
Labels: kind/bug

#91 - Questions about universal variables and polymorphism.

Issue - State: closed - Opened by VincentCheval almost 10 years ago - 17 comments
Labels: kind/discussion

#90 - More examples for the tutorial and regressions

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 8 comments
Labels: component/examples, kind/meta-issue, component/tutorial

#89 - Example: normalization for the STLC via hereditary substitutions

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 11 comments
Labels: component/examples

#88 - FStarDoc: documentation support

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 4 comments
Labels: kind/enhancement, component/documentation

#87 - F* should raise a warning when a pattern match branch is redundant

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 1 comment
Labels: status/duplicate, kind/enhancement

#86 - Inconsistent extraction of Prims.int (should extract to bigint)

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 15 comments
Labels: kind/bug, component/extraction

#85 - Better/proper support for IO effect

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 2 comments
Labels: kind/enhancement, component/dm4free, component/effect-system

#84 - Parsing: what's the harm in naming function type results even when they are not refined?

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 2 comments
Labels: kind/enhancement

#83 - Parsing: do effects need to bind so tightly?

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 1 comment
Labels: kind/question

#82 - Tutorial: use Madoku file fragments + some scripts to make things maintainable

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 3 comments
Labels: kind/enhancement

#81 - Make admit/magic/assume issue a warning

Issue - State: closed - Opened by catalin-hritcu almost 10 years ago - 1 comment
Labels: kind/enhancement, area/error-messages, good first issue, milestone/everest-v1