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

Vcalyx #1844

Closed
wants to merge 56 commits into from
Closed

Vcalyx #1844

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
4f343a9
initial commit
priyasrikumar Jul 20, 2023
9e504b7
add dune and runt to verification workflow
hackedy Jul 20, 2023
8ad4f1b
remove old comment
hackedy Jul 20, 2023
7b3be3e
use checkout@v3 for actions/checkout#1048 fix
hackedy Jul 20, 2023
ca8e216
don't check out twice
hackedy Jul 20, 2023
e89f271
fix coq deps
hackedy Jul 20, 2023
6594a68
really fix coq deps
hackedy Jul 21, 2023
4ded1c7
delete ASTSyntax.v in favor of IRSyntax.v
hackedy Jul 25, 2023
b7995e9
Serialize attributes as an association list
hackedy Jul 25, 2023
c090230
some parser hacking
hackedy Jul 28, 2023
25e7411
fix build
hackedy Aug 1, 2023
981d0c6
sexp program formatting
priyasrikumar Aug 3, 2023
63676de
parser tweaks
priyasrikumar Aug 3, 2023
a266fec
missed cargo fmt
hackedy Sep 13, 2023
ec556c7
parse stdin when no file is specified
hackedy Sep 13, 2023
d299896
runt tweaks
hackedy Sep 13, 2023
3bab848
improve attribute parsing
hackedy Sep 14, 2023
c4130e4
really stupid runt test and parser fixes
hackedy Sep 14, 2023
562b192
missing futils/expect files
hackedy Sep 14, 2023
64208ac
gitignore .swp files littered around by vim
hackedy Sep 14, 2023
7f0b4ac
two more simple runt parsing tests
hackedy Sep 14, 2023
4dd67f9
sundry fixes
hackedy Sep 14, 2023
ad1fef8
get the 3 example programs to parse
hackedy Sep 15, 2023
5a79bc7
Merge branch 'master' into vcalyx-ci
hackedy Sep 18, 2023
e27fdc5
upgrade runt
hackedy Sep 18, 2023
e118830
Minor improvements, workarounds for bad parser
hackedy Sep 18, 2023
c828c41
fix poke to be strictly combinational
hackedy Sep 19, 2023
31b48b3
define is_entrypoint
hackedy Sep 19, 2023
fa78574
some more semantics
hackedy Sep 19, 2023
d4e383a
implement state allocation
hackedy Sep 19, 2023
ae7f203
more in semantics
hackedy Sep 25, 2023
a2fa670
fix parsing of port_refs
hackedy Sep 25, 2023
6c1287e
semantics for std_mem_d1
hackedy Sep 25, 2023
9e64cad
begin on json parsing of memories
hackedy Sep 26, 2023
e536737
JSON memories end to end (still buggy)
hackedy Sep 27, 2023
ef542c0
improve error reporting
hackedy Sep 27, 2023
8c93a7b
implement poke for std_const
hackedy Sep 27, 2023
1fa1e92
work around weird stdpp map issue
hackedy Sep 27, 2023
f31bf27
get basic.futil to evaluate without errors
hackedy Sep 27, 2023
2ea2436
first pass on some vcalyx interpreter fud
hackedy Sep 30, 2023
30d4258
connect fud stages for sexp and vcalyx interp
hackedy Oct 2, 2023
634ea6b
switch from sexprs to lexprs
hackedy Oct 2, 2023
99ff07f
delete .futils files
hackedy Oct 2, 2023
8380363
bug in lexing string literals
hackedy Oct 2, 2023
bb0fae1
some parser debugging
hackedy Oct 2, 2023
cabcaad
fix calyx runt .expect files
hackedy Oct 2, 2023
2797f38
fix some more parsing problems
hackedy Oct 2, 2023
06f52b8
suppress ocamllex error
hackedy Oct 2, 2023
db3e5ad
use ocaml 4.14.1
hackedy Oct 2, 2023
d4f75cb
stubs
hackedy Oct 15, 2023
5b7b259
implement some arithmetic
hackedy Oct 16, 2023
8920555
implement if
hackedy Oct 17, 2023
043b6b2
fix indent
hackedy Oct 17, 2023
852f8b0
rework control intepreter
hackedy Oct 31, 2023
1ffe5d5
fud hacking...
hackedy Jan 10, 2024
27a7f18
Merge branch 'main' into vcalyx-ci
hackedy Jan 11, 2024
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
30 changes: 17 additions & 13 deletions .github/workflows/verification.yml
Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
name: Verification

# Right now, we should only run this check on the vcalyx branch
on:
push:
branches:
- vcalyx
on: [push]

# Ensures that only the latest commit of a PR can execute the actions.
# Useful for cancelling job when a sequence of commits are quickly added.
Expand All @@ -19,27 +15,35 @@ jobs:
container: ghcr.io/cucapra/calyx:latest
steps:
- name: Checkout
uses: actions/checkout@v2
uses: actions/checkout@v3
- name: Get bwrap for opam
run: |
apt-get update -y
apt-get install -y bubblewrap
- name: Set up opam and OCaml 4.13.1
- name: Set up opam and OCaml
uses: ocaml/setup-ocaml@v2
with:
ocaml-compiler: 4.13.1
- name: Checkout commit that triggered run
run: |
git fetch --all
git checkout $GITHUB_SHA
ocaml-compiler: 4.14.1
- name: Install dependencies
run: |
cd vcalyx
opam install dune
opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
opam install coq yojson core core_unix ppx_deriving coq-stdpp coq-ceres
- name: Build with dune

- name: Build Rust
uses: actions-rs/cargo@v1
with:
command: build
args: --features serialize --all --manifest-path /home/calyx/interp/Cargo.toml

- name: Build Coq and OCaml
run: |
cd vcalyx
opam exec -- dune build

- name: Coq Interpreter Runt Tests
run: |
cd vcalyx
runt --diff --only fail
42 changes: 42 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -44,5 +44,47 @@ tests/xilinx/cocotb/**/hdl
sim_build/
results.xml

.vscode/settings.json

# Dune build directory
_build
vcalyx.install
# Github template for Coq .gitignores
.*.aux
.*.d
*.a
*.cma
*.cmi
*.cmo
*.cmx
*.cmxa
*.cmxs
*.glob
*.ml.d
*.ml4.d
*.mli.d
*.mllib.d
*.mlpack.d
*.native
*.o
*.v.d
*.vio
*.vo
*.vok
*.vos
.coq-native/
.csdp.cache
.lia.cache
.nia.cache
.nlia.cache
.nra.cache
csdp.cache
lia.cache
nia.cache
nlia.cache
nra.cache

# vim temporary files
*.sw?

!cider-dap/calyxDebug/package.json
Loading
Loading