Ecosyste.ms: Issues

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

GitHub / PrincetonUniversity/VST issues and pull requests

#809 - Adapt VSTlib to 'Nans' branch of VCFloat

Pull Request - State: closed - Opened by andrew-appel 23 days ago

#808 - merge master into vst_on_iris

Pull Request - State: closed - Opened by mansky1 24 days ago

#807 - Fix issue #789

Pull Request - State: closed - Opened by andrew-appel 28 days ago

#806 - Get 'make all' to work in VST 2.15, 32-bit mode

Pull Request - State: closed - Opened by andrew-appel 29 days ago

#804 - Update vst/lib to VST 2.15 and CompCert 3.15

Pull Request - State: closed - Opened by andrew-appel 30 days ago - 1 comment

#803 - Update makefile and CI for Coq 8.20

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

#802 - Fix a bunch of Coq 8.20 deprecations

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

#801 - _Float16 hack no longer needed after CompCert 3.15

Issue - State: closed - Opened by andrew-appel about 1 month ago - 1 comment

#799 - Adapt to https://github.com/coq/coq/pull/19801

Pull Request - State: closed - Opened by andres-erbsen 3 months ago - 4 comments

#798 - Fix for math-library compatibility on MacOS

Pull Request - State: closed - Opened by andrew-appel 3 months ago

#797 - Prototype of RefinedVST frontend.

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

#796 - Sassign example mostly working

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

#795 - Update github actions artifact to version 4.1.7

Pull Request - State: closed - Opened by andrew-appel 5 months ago

#794 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: closed - Opened by proux01 5 months ago - 5 comments

#793 - Bump actions/download-artifact from 2 to 4.1.7 in /.github/workflows

Pull Request - State: closed - Opened by dependabot[bot] 5 months ago - 2 comments
Labels: dependencies

#792 - Trying to prove properties about eBPF programs (Clightgen issue)

Issue - State: closed - Opened by swarnpriya 5 months ago - 7 comments

#791 - can frame affine props in lithium

Pull Request - State: closed - Opened by rinshankaihou 6 months ago

#790 - More typing example

Pull Request - State: closed - Opened by rinshankaihou 6 months ago

#789 - repr_inj_signed64 has incorrect bounds.

Issue - State: closed - Opened by roconnor-blockstream 6 months ago

#788 - R vst

Pull Request - State: closed - Opened by rinshankaihou 6 months ago

#787 - Adapt w.r.t. coq/coq#19228.

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

#786 - merge VST into OpenMP

Pull Request - State: closed - Opened by ducthann 6 months ago - 1 comment

#785 - port everything for lithium

Pull Request - State: closed - Opened by rinshankaihou 6 months ago

#784 - port some automation related files and a bit of program.v

Pull Request - State: closed - Opened by rinshankaihou 6 months ago

#783 - updated mailbox to use new lock_t

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

#782 - mailbox broken: typedef with/without *

Issue - State: closed - Opened by andrew-appel 7 months ago - 2 comments

#781 - Port VST 2.x to CompCert master

Pull Request - State: closed - Opened by andrew-appel 7 months ago - 3 comments

#780 - Vstoniris

Pull Request - State: closed - Opened by sgacs 7 months ago

#779 - CompCert planned change: adding a `Mbool` memory chunk

Issue - State: closed - Opened by xavierleroy 8 months ago - 6 comments

#778 - simpl_classes.v

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

#777 - build: support PROFILING and TIMED like coq_makefile

Pull Request - State: closed - Opened by SkySkimmer 8 months ago

#776 - Vst on iris

Pull Request - State: closed - Opened by sgacs 8 months ago

#775 - Create simpl_classes.v

Pull Request - State: closed - Opened by sgacs 8 months ago

#774 - Wrap functor facts in abstract lemmas.

Pull Request - State: closed - Opened by ppedrot 9 months ago

#773 - In VST 3.0beta2, normalize1 tactic

Issue - State: open - Opened by andrew-appel 9 months ago - 6 comments

#772 - check_parameter_vals should have lazymatch

Issue - State: open - Opened by andrew-appel 9 months ago

#769 - verif_incr should prove that it restores an uninitialized counter

Issue - State: open - Opened by andrew-appel 10 months ago - 1 comment

#766 - change_compspecs adjusts cstring

Pull Request - State: closed - Opened by andrew-appel 10 months ago

#764 - cstring should not need a compspecs argument

Issue - State: closed - Opened by andrew-appel 10 months ago - 2 comments

#763 - mkVSU external function check does not give useful error message

Issue - State: closed - Opened by andrew-appel 10 months ago - 3 comments

#762 - inhabited_value doesn't really work well

Issue - State: open - Opened by andrew-appel 11 months ago

#761 - Adapt to Coq 8.19 and CompCert 3.13.1

Pull Request - State: closed - Opened by andrew-appel 11 months ago

#760 - Please create a tag for Coq 8.19 in Coq Platform 2024.01

Issue - State: closed - Opened by rtetley 11 months ago - 4 comments

#758 - Improved, more precise fix for issue #756

Pull Request - State: closed - Opened by andrew-appel 11 months ago

#756 - localize / entailer_for_load_tac / unlocalize / Coq 8.17

Issue - State: closed - Opened by andrew-appel 11 months ago - 11 comments

#755 - VST on Iris

Pull Request - State: open - Opened by mansky1 11 months ago - 10 comments

#754 - Fix issue #745

Pull Request - State: closed - Opened by andrew-appel 11 months ago

#752 - solve_store_rule_evaluation

Issue - State: closed - Opened by andrew-appel 11 months ago - 1 comment

#751 - Improvements in deadvars

Issue - State: closed - Opened by andrew-appel 11 months ago

#750 - forward_call takes a long time

Issue - State: closed - Opened by rigille 12 months ago - 2 comments

#749 - data_at_int_or_ptr_int share

Issue - State: closed - Opened by andrew-appel about 1 year ago

#748 - solve_load_rule_evaluation @proj_reptype

Issue - State: closed - Opened by andrew-appel about 1 year ago - 3 comments

#747 - Adapt to https://github.com/coq/coq/pull/18164

Pull Request - State: closed - Opened by proux01 about 1 year ago - 2 comments

#745 - overbroad match in try_conjuncts

Issue - State: closed - Opened by andrew-appel about 1 year ago

#744 - fail levels in forward_if'_new

Issue - State: closed - Opened by andrew-appel about 1 year ago

#743 - Unnecessary premise in `Lemma field_at_app`

Issue - State: closed - Opened by MSoegtropIMC about 1 year ago

#742 - Tactic & example fixes

Pull Request - State: closed - Opened by rinshankaihou about 1 year ago

#741 - repr_inj handles int64 compares better; updated submodules

Pull Request - State: closed - Opened by andrew-appel over 1 year ago

#740 - VSTlib: adapt to gentype branch of vcfloat

Pull Request - State: closed - Opened by andrew-appel over 1 year ago

#739 - Adjusted SC_tac, adjusted change_compspecs warning message, store_tac

Pull Request - State: closed - Opened by andrew-appel over 1 year ago - 2 comments

#738 - do {S} while (0)

Issue - State: open - Opened by andrew-appel over 1 year ago

#737 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#736 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#735 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#734 - Useful lemma for users: nonempty_writable_glb

Issue - State: closed - Opened by andrew-appel over 1 year ago

#733 - vst_on_iris floyd fixes

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#732 - New lemma data_at_conflict_glb

Pull Request - State: closed - Opened by andrew-appel over 1 year ago - 1 comment

#731 - removed a call to try simple apply eq_refl in SC_tac

Pull Request - State: closed - Opened by lennartberinger over 1 year ago - 1 comment

#730 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#729 - Some observations on `forward_call` performance

Issue - State: closed - Opened by MSoegtropIMC over 1 year ago - 21 comments

#727 - Please create a tag for Coq 8.18 in Coq Platform 2023.10

Issue - State: closed - Opened by rtetley over 1 year ago - 5 comments

#726 - Have coqdep use DEPFLAGS not COQFLAGS

Pull Request - State: closed - Opened by proux01 over 1 year ago - 3 comments

#725 - Honor COQEXTRAFLAGS env var

Pull Request - State: closed - Opened by proux01 over 1 year ago - 1 comment

#724 - Added Lemma init_data_tarray_tint

Pull Request - State: closed - Opened by lennartberinger over 1 year ago

#723 - don't clear in quick_typecheck3; closes #722

Pull Request - State: closed - Opened by andrew-appel over 1 year ago

#722 - quick_typecheck3 should not clear

Issue - State: closed - Opened by andrew-appel over 1 year ago - 2 comments

#721 - sumarray fixes

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#720 - Vst on iris

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#719 - verif_append2.v done

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#718 - fix lemma statement

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#717 - bug fixes in floyd

Pull Request - State: closed - Opened by rinshankaihou over 1 year ago

#714 - Pass `COQEXTRAFLAGS` through to `coqc`

Pull Request - State: closed - Opened by JasonGross over 1 year ago - 1 comment

#712 - Ltac2 local2ptree

Pull Request - State: open - Opened by MSoegtropIMC over 1 year ago - 14 comments

#711 - fix issues #700 and #702

Pull Request - State: closed - Opened by andrew-appel over 1 year ago

#709 - Pass stderr through calc_install_files when commands fail

Pull Request - State: open - Opened by JasonGross over 1 year ago - 2 comments