diff options
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/SMTrans/SMTrans.v | 18 |
3 files changed, 25 insertions, 6 deletions
@@ -1,28 +1,28 @@ COMPCERTRECDIRS := lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight \ MenhirLib cparser -COMPCERTCOQINCLUDES := $(foreach d, $(RECDIRS), -R lib/CompCert/$(d) compcert.$(d)) +COMPCERTCOQINCLUDES := $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) COQINCLUDES := -R src/Common CoqUp.Common -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction $(COMPCERTCOQINCLUDES) COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := "$(COQBIN)coq_makefile" -COQUPDIRS := Common Driver Verilog +COQUPDIRS := SMTrans Common Driver Verilog VS := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) -.PHONY: all install coq clean +.PHONY: all install proof clean all: (cd lib/CompCert && ./configure x86_64-linux) $(MAKE) -C lib/CompCert all - $(MAKE) coq + $(MAKE) proof $(MAKE) compile install: $(MAKE) -f Makefile.coq install -coq: Makefile.coq +proof: Makefile.coq $(MAKE) -f Makefile.coq extraction: src/Extraction/STAMP @@ -40,7 +40,7 @@ src/Extraction/STAMP: Makefile.coq: @echo "COQMAKE Makefile.coq" - @$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq + $(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq clean:: Makefile.coq $(MAKE) -f Makefile.coq clean diff --git a/_CoqProject b/_CoqProject index 54ff493..2ac5d91 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction +-R src/SMTrans CoqUp.SMTrans -R lib/CompCert/lib compcert.lib -R lib/CompCert/common compcert.common diff --git a/src/SMTrans/SMTrans.v b/src/SMTrans/SMTrans.v new file mode 100644 index 0000000..f651544 --- /dev/null +++ b/src/SMTrans/SMTrans.v @@ -0,0 +1,18 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + |