FStarLang/FStar issues and pull requests

#3565 - Introduce --ocamlenv

Pull Request - State: open - Opened by mtzguido about 1 month ago

#3564 - Some refactoring about include paths, finding, locate, etc

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3563 - Tactics: refactor a bit to avoid a cycle

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 2 comments

#3562 - Fix some missing branches for ShowOptions

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3561 - fix(pp): char and string literals

Pull Request - State: closed - Opened by W95Psp about 1 month ago - 1 comment

#3560 - `ToDocument`: `char` values are printed wrongly

Issue - State: closed - Opened by W95Psp about 1 month ago - 2 comments

#3559 - Restricted open: fix shadowing

Pull Request - State: closed - Opened by W95Psp about 1 month ago - 2 comments

#3558 - Fix restricted open for constructors of type with indices

Pull Request - State: closed - Opened by W95Psp about 1 month ago

#3557 - Moving compiler sources into the FStarC namespace

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 3 comments

#3556 - ulib: move a type into stubs

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3555 - Preparing to use this F* as stage0

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 2 comments

#3554 - Revert "CI: point karamel to patched branch"

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3553 - Errors: Introducing '--message_format github', for github actions

Pull Request - State: open - Opened by mtzguido about 1 month ago - 2 comments

#3552 - Make FStar.IO an interface

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3551 - Tidying up a bit of FStar.All and FStar.Compiler.Effect

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3550 - Parser.Dep: emitting a small header in the .depend

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3549 - A header comment in .depend, some library tweaks

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 2 comments

#3548 - Make the default effect in --MLish configurable

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3547 - docker dev container: explicit platform, install pkg-config

Pull Request - State: open - Opened by amosr about 1 month ago - 1 comment

#3546 - Update hints

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3545 - (Warning 328) - Global binding .. is recursive but not used in its body

Issue - State: closed - Opened by briangmilnes about 1 month ago - 2 comments

#3544 - Do not print reveal or hide by default when resugaring

Pull Request - State: closed - Opened by nikswamy about 1 month ago

#3543 - Use annotated tags for releases

Issue - State: open - Opened by mtzguido about 1 month ago

#3542 - Extraction: not extracting tactics unless backend is Plugin

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3541 - Improving a few errors

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3540 - ulib: reducing some warnings

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3539 - Tc: make other components of guards also catenable lists

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3538 - Introducing a generic catenable list

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3537 - Some improvements wrt to plugins

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3536 - Syntax accepted in emacs language server but not on the command line for a depends run

Issue - State: open - Opened by briangmilnes about 1 month ago

#3535 - Makefile: fix clean rule

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3534 - Inference does not know about fundeps

Issue - State: open - Opened by mtzguido about 1 month ago

#3533 - Autoload extension plugins

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3532 - Many fixes to resugaring

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3531 - Fixing #3530

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3530 - Parsing error with parenthesized explicit arg with attributes

Issue - State: closed - Opened by mtzguido about 1 month ago

#3529 - Options: --already_cached should not consider the current module

Pull Request - State: closed - Opened by mtzguido about 1 month ago - 1 comment

#3528 - Extraction: reduce krml output unless -d/--debug

Pull Request - State: open - Opened by mtzguido about 1 month ago - 3 comments

#3527 - Options: display short options in help, introduce `-d` for general debugging info

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3526 - Nits

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3525 - Some fixes in range module

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3524 - Some nits

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3523 - Desugaring: simplify desugaring for App, and respect textual order

Pull Request - State: closed - Opened by mtzguido about 1 month ago

#3522 - Definition not found with restricted open

Issue - State: closed - Opened by mtzguido about 1 month ago - 2 comments

#3521 - Represent implicits as a tree instead of a list to make conjoining them constant time

Pull Request - State: closed - Opened by nikswamy about 1 month ago - 2 comments

#3520 - Extraction list of bytes produce incorrect F# code

Issue - State: open - Opened by kant2002 about 1 month ago

#3519 - Replace must_erase_during_extraction with erasable.

Pull Request - State: open - Opened by gebner about 2 months ago

#3518 - Fixing mistaken erasure of effectful type applications

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

#3517 - A better error when z3 cannot be started

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

#3516 - Warning 337 does not produce a line number in the language server

Issue - State: open - Opened by briangmilnes about 2 months ago

#3515 - Reset gensym for predictable names and better query caching

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

#3514 - Util: fix mkdir for trailing slashes

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

#3513 - check-world: add mls-star

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

#3512 - Fix library finding in binary package

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

#3511 - CI should test binary package

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

#3510 - let lemmas in fsti reported missing after val missing error 98

Issue - State: open - Opened by briangmilnes about 2 months ago

#3509 - Main: adding --locate, --locate_lib, --locate_ocaml

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

#3508 - Proving `int =!= (int -> Dv int)`

Issue - State: open - Opened by mtzguido about 2 months ago - 2 comments
Labels: kind/question

#3507 - Add a cast from size_t to uint64_t

Pull Request - State: closed - Opened by tahina-pro about 2 months ago

#3506 - Main: Add --list_plugins option

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

#3505 - Revise the SMT encoding of top-level prop definitions

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

#3504 - `FStar.Reflection.Typing.subst_term` extracts to dangerous code

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

#3503 - Bump dune version dependency.

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

#3502 - check-world: some documentation

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

#3501 - Some tactics and MkProjectors improvements

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

#3500 - Arrow one

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

#3499 - check-world: run hacl on github runners, avoid stupid uid issue

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

#3498 - Bad expected type on typeclass constraint

Issue - State: open - Opened by mtzguido about 2 months ago
Labels: kind/bug

#3497 - A comment about bytecode version of fstar-lib

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

#3496 - FStar.IO could do with a flush

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

#3495 - Restore bytecode fstarlib

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

#3494 - An illegal record field is not 'redundant'

Issue - State: open - Opened by briangmilnes about 2 months ago

#3493 - Error 152 should not be fatal

Issue - State: open - Opened by briangmilnes about 2 months ago

#3492 - Warning for shadowing format needs to be more like warning for emacs

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

#3491 - Add message format cli option

Pull Request - State: closed - Opened by W95Psp about 2 months ago - 6 comments

#3490 - Extraction does not write .checked, this is a performance issue

Issue - State: closed - Opened by briangmilnes about 2 months ago - 1 comment

#3489 - Misc tactic improvements

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

#3488 - Improve publishing Nuget properties

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

#3487 - Errors: implementing error bound

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

#3486 - Resugar: make sure to compress before checking for machine integers

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

#3485 - F* can't find one enum constructor after it found an isomorphic one

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

#3484 - Introduce doc/ref for development notes, document a bit about coercions

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

#3483 - tactics: move concatMap to FStar.Tactics.Util

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

#3482 - Extraction: print mllb_attrs

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

#3481 - Adding #show-options to print current option flags

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

#3480 - Warn on missing pop options

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

#3479 - Moving prims.fst to Prims.fst

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

#3478 - Fixing #3474: making sure module names match filenames in case

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

#3477 - Did you miss a semicolon?

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

#3476 - Z3 4.8.5 segfaults on aarch64 linux

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

#3475 - Extraction does not reduce projectors in types

Issue - State: closed - Opened by gebner 2 months ago - 1 comment

#3474 - Case confusion in module name

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

#3473 - Extraction drops calls to divergent functions

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

#3472 - Extraction.Krml: pp patterns

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

#3471 - Tweaks to default pretty instances.

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

#3470 - Extraction.Krml: pretty printing

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

GitHub / FStarLang/FStar issues and pull requests