Ecosyste.ms: Issues

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

GitHub / fstarlang/pulse issues and pull requests

#263 - Add ghost slice splitting

Pull Request - State: closed - Opened by tahina-pro 11 days ago

#262 - Rename fuel to budget.

Pull Request - State: closed - Opened by gebner 12 days ago

#261 - A library for shifts (duplicable trades)

Pull Request - State: closed - Opened by nikswamy 12 days ago

#260 - Fueled interpreter.

Pull Request - State: closed - Opened by gebner 12 days ago

#259 - A bit of helping in Pulse.Lib.Task.await

Pull Request - State: closed - Opened by nikswamy 13 days ago

#258 - Move buy loop to lib

Pull Request - State: closed - Opened by gebner 13 days ago

#257 - Replace par primitive by fork.

Pull Request - State: closed - Opened by gebner 13 days ago

#256 - Buy a single credit at a time.

Pull Request - State: closed - Opened by gebner 13 days ago

#255 - Task.with_pool

Pull Request - State: closed - Opened by gebner 13 days ago

#254 - Keep track of a potentially erased fuel quantity.

Pull Request - State: closed - Opened by gebner 13 days ago

#253 - Rename NuPool to Pulse.Lib.Task

Pull Request - State: closed - Opened by gebner 14 days ago

#252 - Add missing copyright headers.

Pull Request - State: closed - Opened by gebner 14 days ago

#251 - Require duplicability in gvar.

Pull Request - State: closed - Opened by gebner 14 days ago

#250 - Impredicative invariants using indirection theory

Pull Request - State: closed - Opened by gebner 14 days ago

#249 - Implement Pulse.Lib.SeqMatch

Pull Request - State: closed - Opened by tahina-pro 15 days ago

#248 - In-place merge sort for slices

Pull Request - State: open - Opened by tahina-pro 18 days ago - 1 comment

#247 - Remove `slice_pair` in favor of standard F* pairs

Pull Request - State: closed - Opened by tahina-pro 28 days ago - 3 comments

#246 - (WIP) Staged build

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

#245 - In-place array merge sort

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

#244 - Extra lemmas about SeqMatch, Trade

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

#243 - Rename FStar.Stubs.Pprint -> FStar.Pprint

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

#242 - First pass for the dataset extraction from the pulse

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

#241 - Correctly extract inner ghost functions.

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

#240 - snap for F* change

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

#239 - snap for F* change

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

#238 - Fix postcondition of `Pulse.Lib.Slice.Util.split_trade`

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

#237 - Moving FStar->FStarC

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

#236 - Slice.subslice

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

#235 - Use gensym from F*

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

#234 - Annotated function types with more than 3 parameters fail in non-interactive mode

Issue - State: closed - Opened by gebner about 2 months ago - 4 comments

#233 - All: remove --load_cmxs options, autoload takes care of it

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

#232 - Making `pts_to` a method

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

#231 - Use --ext __unrefine everywhere

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

#230 - Update parser after F* change

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

#229 - Box: use a newtype in the model

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

#228 - SyntaxExtension: handle ticks in declarations

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

#227 - Tick order

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

#226 - declarations do not support tick variables

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

#225 - A model for Rust slices (and C array pointers)

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

#224 - snapshot for gensym change

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

#223 - Inference with nested refinements

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

#222 - `with` takes arg qualifiers

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

#221 - A couple of examples: binary search and contiguous sub sequence

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

#220 - Support more pulse in pulse2rust

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

#219 - pulse2rust omits parentheses

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

#218 - Support calc proofs

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

#217 - Extraction ignores preconditions

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

#215 - Fix #172

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

#214 - Do not recheck postconditions for lemmas

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

#213 - Setting the error bound

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

#212 - lib: add missing fstar.include

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

#211 - Parser.ml: handle PRAGMA_SHOW_OPTIONS token

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

#210 - snap+parser update after F* changes

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

#209 - Implement extraction via translation to Div-terms

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

#207 - Some improvements to tracing/printing

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

#206 - Bad error range when a refinement check fails

Issue - State: open - Opened by nikswamy 3 months ago

#204 - Env: filtering units from environment print

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

#203 - Parser/Syntax: support assume keyword, desugaring to assume_

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

#202 - Revert "Extraction: mark everything CInline"

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

#201 - Add fstar.includes

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

#200 - Error api fixes

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

#199 - Bump to OCaml 4.14

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

#198 - Typing: squash_of eq2 is always at univ zero

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

#197 - Factoring out the snapshot diff check

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

#196 - Fix after parser changes

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

#195 - Checker.Match: use a tactic to rewrite match equalities

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

#194 - CI fixes

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

#193 - Pulse.Lib.Array.Core: pts_to_range_share, gather

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

#192 - lib: tuples are non-informative too

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

#191 - Patterns in letbindings

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

#190 - Introduce --ext 'pulse:trace' to print contexts before every step

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

#189 - Reduce dummy ranges.

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

#188 - Extraction: mark everything CInline

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

#187 - Fixing config.json for new src/syntax/print directory

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

#184 - snap for F* changes

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

#183 - Type-class implicits are not eager enough

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

#182 - Extraction: make sure to erase local ghost functions

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

#181 - Need spurious bind to make function check

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

#180 - Fixes for F* sequence literals

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

#179 - Assume (pure part of) pre in typechecking post

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

#178 - Fixes for FStarLang/FStar#3385

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

#177 - Bad error when forgetting to let-bind

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

#175 - Fix Pulse for changes in F* PR 3369

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

#174 - Bad range when mistaking type

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

#173 - Fail with a proper range

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

#172 - Parsing error with #lang-pulse and pipe operator

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

#171 - Missing closing substitution in desugar; fix ranges when opening a variable

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

#170 - Fix reporting of ranges in desugaring errors

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

#166 - Pulse and `inline_for_extraction`

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

#151 - Remove admitted and unused invlist_reveal function.

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

#150 - Replace assume by assert

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

#110 - `rewrite each` does not require equality

Issue - State: open - Opened by mtzguido 5 months ago - 1 comment
Labels: bug

#100 - Ill-typed spec is accepted

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

#99 - Add a Pulse module, so we can just `open Pulse`

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