Skip to content
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.

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

Sound #41

Draft
wants to merge 40 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
5263518
Remove second pass in minimal/sound variant
tlringer Mar 20, 2021
6175785
Remove extra functions
tlringer Mar 20, 2021
91d1664
Merge branch 'master' into sound
tlringer Mar 24, 2021
82d173d
Threading state
Apr 9, 2021
4a709fa
Threading correct goal
May 17, 2021
672cddf
Decompiler errors default to using apply.
May 24, 2021
9e85305
Passing list of previously used tactics into get_hints
Jun 22, 2021
4838908
base infrastructure change with submodules added in git
efirst Sep 7, 2021
11f8859
minimize dependencies for pyml
tlringer Sep 7, 2021
0ae0d3b
minimize dependencies in mli file
tlringer Sep 7, 2021
b25c926
Try to remove Stdcompat from pyml
tlringer Sep 7, 2021
de1a080
add rectypes to Makefile
tlringer Sep 7, 2021
3d16d48
finish inlining 4.08 OCaml functions..
tlringer Sep 7, 2021
91f289f
Update build to work with pyml
tlringer Sep 7, 2021
32206d1
Move SerAPI to 8.9 branch
tlringer Sep 7, 2021
a144721
get most of SerAPI working, but need Sexplib
tlringer Sep 7, 2021
fbd5c87
get sexplib working; opening theory throws error
tlringer Sep 7, 2021
c9bb6e2
try to port to dune
tlringer Sep 8, 2021
0ef071a
Get basic build working with dune
tlringer Sep 8, 2021
37ffabc
Attempt to build theory with dune
tlringer Sep 8, 2021
7099ed4
use older dune
tlringer Sep 8, 2021
2a57d26
annoying things
tlringer Sep 8, 2021
bdfa573
idk
tlringer Sep 8, 2021
3fb69de
Emilio is amazing
tlringer Sep 16, 2021
e1f7bf4
Remove comments
tlringer Sep 16, 2021
a9fd906
Doesn't need Makefile
tlringer Sep 16, 2021
92d938a
minor tweaks
tlringer Sep 17, 2021
aa94568
use Lymp instead, get building
tlringer Sep 21, 2021
a5bdacb
ignore .merlin files
tlringer Sep 21, 2021
b31af22
don't restrict mode
tlringer Sep 21, 2021
c067347
Why did that one work?
tlringer Sep 21, 2021
20dbd0d
Right, so this file is broken with some weird error loading the plugin
tlringer Sep 21, 2021
a693ee3
Remove duplicate coq.plugins.ltac
tlringer Sep 21, 2021
2cc029a
Update README.md
tlringer Sep 21, 2021
0c6ecc4
Update LICENSE
tlringer Sep 21, 2021
4e907d5
Update README.md
tlringer Sep 21, 2021
281ba24
integration. need to add model, sexpcache, and check whether all othe…
efirst Oct 5, 2021
1776cb1
removed some DS stores hopefully
efirst Oct 5, 2021
740df17
fixing modules
efirst Oct 15, 2021
52fad76
adding in sexp
efirst Oct 19, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -21,5 +21,6 @@ plugin/Makefile.coq
plugin/Makefile.conf
plugin/Makefile
plugin/.merlin
*.merlin
*.out
_opam
Empty file added .gitmodules
Empty file.
2 changes: 1 addition & 1 deletion LICENSE
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
The MIT License (MIT)

Copyright (c) 2019 Talia Ringer, Nate Yazdani
Copyright (c) 2021 PUMPKIN PATCH Team

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
4 changes: 3 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ See [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) and [DEVOID](https:

## Guide

This code guide is out of date and needs to be updated due to the switch to use Dune.

* [LICENSE](/LICENSE): License
* [README.md](/README.md): You are here!
* [build.sh](/build.sh): Build script for example plugin
Expand All @@ -32,7 +34,7 @@ See [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) and [DEVOID](https:

## Contributors

This library was developed by Talia Ringer, Nate Yazdani, and RanDair Porter.
This library was developed by Talia Ringer, Nate Yazdani, RanDair Porter, and Emily First. Probably none of it would build without Emilio's help.

## Licensing

Expand Down
97 changes: 0 additions & 97 deletions _CoqProject

This file was deleted.

9 changes: 7 additions & 2 deletions build.sh
Original file line number Diff line number Diff line change
@@ -1,2 +1,7 @@
coq_makefile -f _CoqProject -o Makefile
make clean && make && make install
opam pin dune 2.7.1
opam pin coq-serapi 8.9.0+0.6.1
opam install lymp
dune clean
dune build @all
dune build @all
dune install
19 changes: 19 additions & 0 deletions coq-plugin-lib.opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
synopsis: "Coq Plugin Library"
description: "Coq Plugin Library"
name: "coq-plugin-lib"
opam-version: "2.0"
maintainer: "[email protected]"
authors: "Talia Ringer"
homepage: "https://github.com/uwplse/coq-plugin-lib"
bug-reports: "https://github.com/uwplse/coq-plugin-lib"
dev-repo: "git+https://github.com/uwplse/coq-plugin-lib"
license: "MIT"
doc: "https://github.com/uwplse/coq-plugin-lib"

depends: [
"ocaml" { = "4.07.1+flambda" }
"coq" { = "8.9.1" }
"dune" { build & >= "1.9.0" & <= "2.7.1" }
]

build: [ "dune" "build" "-p" name "-j" jobs ]
3 changes: 3 additions & 0 deletions dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(env
(dev (flags (:standard -rectypes -w -8-33-3-27-28-32)))
(release (flags (:standard -rectypes -w -8-33-3-27-28-32))))
3 changes: 3 additions & 0 deletions dune-project
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
(lang dune 2.7.1)
(using coq 0.2)
(name coq-plugin-lib)
8 changes: 8 additions & 0 deletions src/coq/constants/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
(library
(name constants)
(public_name coq-plugin-lib.constants)
(libraries
coq-plugin-lib.inference
coq-plugin-lib.termutils
coq.kernel)
(wrapped false))
Loading