Permalink
Browse files

Move characteristic/examples to top-level

Closes issue #316
  • Loading branch information...
xrchz committed Sep 28, 2017
1 parent cef6656 commit 2d4728905a58811ef8a61a764af76c01e02f0812
Showing with 74 additions and 48 deletions.
  1. +0 −40 characteristic/examples/compilation/Holmakefile
  2. +0 −5 characteristic/examples/compilation/proofs/Holmakefile
  3. +3 −3 developers/build-sequence
  4. +26 −0 examples/Holmakefile
  5. 0 {characteristic → }/examples/catProgScript.sml
  6. 0 {characteristic → }/examples/compilation/.gitignore
  7. +40 −0 examples/compilation/Holmakefile
  8. 0 {characteristic → }/examples/compilation/catCompileScript.sml
  9. 0 {characteristic → }/examples/compilation/diffCompileScript.sml
  10. 0 {characteristic → }/examples/compilation/echoCompileScript.sml
  11. 0 {characteristic → }/examples/compilation/grepCompileScript.sml
  12. 0 {characteristic → }/examples/compilation/helloCompileScript.sml
  13. 0 {characteristic → }/examples/compilation/helloErrCompileScript.sml
  14. 0 {characteristic → }/examples/compilation/patchCompileScript.sml
  15. +5 −0 examples/compilation/proofs/Holmakefile
  16. 0 {characteristic → }/examples/compilation/proofs/catProofScript.sml
  17. 0 {characteristic → }/examples/compilation/proofs/diffProofScript.sml
  18. 0 {characteristic → }/examples/compilation/proofs/echoProofScript.sml
  19. 0 {characteristic → }/examples/compilation/proofs/grepProofScript.sml
  20. 0 {characteristic → }/examples/compilation/proofs/helloProofScript.sml
  21. 0 {characteristic → }/examples/compilation/proofs/patchProofScript.sml
  22. 0 {characteristic → }/examples/compilation/proofs/sortProofScript.sml
  23. 0 {characteristic → }/examples/compilation/sortCompileScript.sml
  24. 0 {characteristic → }/examples/diffProgScript.sml
  25. 0 {characteristic → }/examples/diffScript.sml
  26. 0 {characteristic → }/examples/echoProgScript.sml
  27. 0 {characteristic → }/examples/grepProgScript.sml
  28. 0 {characteristic → }/examples/helloErrProgScript.sml
  29. 0 {characteristic → }/examples/helloProgScript.sml
  30. 0 {characteristic → }/examples/insertSortProgScript.sml
  31. 0 {characteristic → }/examples/lcsScript.sml
  32. 0 {characteristic → }/examples/patchProgScript.sml
  33. 0 {characteristic → }/examples/queueProgScript.sml
  34. 0 {characteristic → }/examples/quicksortProgScript.sml
  35. 0 {characteristic → }/examples/sortProgScript.sml
  36. 0 {characteristic → }/examples/stackProgScript.sml

This file was deleted.

Oops, something went wrong.

This file was deleted.

Oops, something went wrong.
@@ -67,9 +67,9 @@ candle/standard/opentheory
compiler/benchmarks
# other examples
characteristic/examples
characteristic/examples/compilation
characteristic/examples/compilation/proofs
examples
examples/compilation
examples/compilation/proofs
# tests
translator/okasaki-examples
View
@@ -0,0 +1,26 @@
INCLUDES = ../characteristic ../basis ../translator ../misc $(HOLDIR)/examples/formal-languages/regular ../semantics
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = ../characteristic/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
PRE_BARE_THYS1 = basisProgTheory
PRE_BARE_THYS3 = cfTacticsBaseLib cfTacticsLib
BARE_THYS1 = $(patsubst %,../basis/%,$(PRE_BARE_THYS1))
BARE_THYS3 = $(patsubst %,../characteristic/%,$(PRE_BARE_THYS3))
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(patsubst %,%.uo,$(BARE_THYS3)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS1) $(BARE_THYS3)
endif
@@ -0,0 +1,40 @@
INCLUDES = .. ../../misc ../../basis ../../compiler
CLINE_OPTIONS = -j1 --qof
TARGETS = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
all: $(TARGETS)
.PHONY: all
ifndef CC
CC=gcc
endif
cake_cat: cat.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_grep: grep.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_patch: patch.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_diff: diff.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_hello: hello.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_sort: sort.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_echo: echo.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
cake_helloErr: helloErr.S ../../basis/basis_ffi.o
$(CC) $< ../../basis/basis_ffi.o $(GCCFLAGS) -o $@
exec: cake_cat cake_grep cake_patch cake_diff cake_hello cake_sort cake_echo cake_helloErr
ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = ../../compiler/heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
BARE_THYS = ../../compiler/compilationLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS)) $(PARENT_HOLHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS)
endif
@@ -0,0 +1,5 @@
INCLUDES = ../../../semantics/proofs ../../../misc .. ../.. ../../../compiler/backend/proofs ../../../compiler/encoders/x64/proofs ../../../compiler/backend/x64/proofs
CLINE_OPTIONS = -j1 --qof
ifdef POLY
HOLHEAP=../heap
endif
File renamed without changes.
File renamed without changes.

0 comments on commit 2d47289

Please sign in to comment.