Use clean-test-properties in CI

.gitignore

@@ -17,4 +17,6 @@ cloogle.log
 db/storage/
 cache
 
-test/builtin_syntax
+backend/test/builtin_syntax
+_Tests/
+_Tests.*

.gitlab-ci.yml

@@ -2,19 +2,15 @@ variables:
   GIT_SUBMODULE_STRATEGY: recursive
 
 stages:
-  - check
+  - test
   - build
 
-style syntax documentation:
-  stage: check
+test:
+  stage: test
   image: camilstaps/clean:nightly
-  only:
-    changes:
-      - backend/Builtin/Syntax.icl
   script:
-    - cd backend
-    - ./install_clean.sh
-    - cd ../test
+    - . ./backend/install_clean_vars.sh
+    - install_clean.sh 'base lib-dynamics lib-gast lib-platform test test-properties'
     - make test
 
 backend:

Makefile

+CLM:=clm
+BACKEND_LIBS:=\
+	-I backend\
+	-I backend/Cloogle\
+	-I backend/Cloogle/libcloogle\
+	-I backend/Cloogle/CleanRegex\
+	-IL Platform
+CLMFLAGS:=$(BACKEND_LIBS) -nr -nt
+
+BACKEND_BIN:=builtin_syntax
+BACKEND_TEST:=$(addprefix test_,$(BACKEND_BIN))
+
+test: $(BACKEND_TEST) test_properties
+
+$(BACKEND_TEST): test_%: backend/test/%
+	./$<
+
+$(addprefix backend/test/,$(BACKEND_BIN)): .FORCE
+	$(CLM) -I $(dir $@) $(CLMFLAGS) $(notdir $@) -o $@
+
+test_properties: .FORCE
+	cleantest \
+		--hide start \
+		--run testproperties \
+		$(addprefix -O ,-d backend $(BACKEND_LIBS) -P OutputTestEvents -r)
+
+.FORCE:
+
+.PHONY: test .FORCE

backend/Builtin/Syntax.dcl

 definition module Builtin.Syntax
 
+/**
+ * @property-bootstrap
+ *   import StdEnv
+ *   from Data.Func import mapSt
+ *   import Data.List
+ *   import Text
+ *   import Regex
+ *   from Cloogle.API import :: SyntaxExample{..}
+ *   import Cloogle.DB
+ *
+ *   // ggen isn't usually used, but required to satisfy constraints
+ *   ggen{|SyntaxEntry|} _ = []
+ *   derive genShow SyntaxEntry, SyntaxExample, CleanLangReportLocation, Regex, Maybe, GroupId
+ *   gPrint{|SyntaxEntry|} se ps = gPrint{|*|} se.syntax_title ps
+ *
+ *   example_lines :: !SyntaxEntry -> [String]
+ *   example_lines se = concatMap (split "\n")
+ *     [replaceSubString "\t" "    " e.example \\ e <- se.syntax_examples]
+ *
+ * @property-test-generator list: SyntaxEntry
+ *   builtin_syntax
+ */
+
 from Cloogle.DB import :: SyntaxEntry
 
+/**
+ * @property has examples: A.se :: SyntaxEntry:
+ *   not (isMember se.syntax_title ["array update", "record update"])
+ *     ==> not (isEmpty se.syntax_examples)
+ *
+ * @property comment alignment (at most two different levels): A.se :: SyntaxEntry:
+ *   length (removeDup comment_columns) < 3
+ *   where
+ *     comment_columns = filter ((<>) -1) [indexOf "//" l \\ l <- example_lines se]
+ *
+ * @property spaces around comment markers: A.se :: SyntaxEntry:
+ *   isEmpty (filter bad (example_lines se))
+ *   where
+ *     bad s = case indexOf "//" s of
+ *       -1 -> False
+ *       i  -> s.[i-1] <> ' ' || s.[i+2] <> ' '
+ *
+ * @property spaces in list comprehensions: A.se :: SyntaxEntry:
+ *   isEmpty (filter bad (example_lines se))
+ *   where
+ *     bad s
+ *     # s = replaceSubString "'\\\\'" "" s // special case for '\\' in basic_values
+ *     # (results,_) = mapSt check ["<|-","<-:","<-","\\\\"] s
+ *     = or results
+ *
+ *     check op s
+ *     # new = replaceSubString (" " +++ op +++ " ") "" s
+ *     = (indexOf op new >= 0, new)
+ */
 builtin_syntax :: [SyntaxEntry]

backend/Builtin/Syntax.icl

@@ -164,7 +164,10 @@ bs_comments =
 	, syntax_code          = ["// ...", "/* ... */"]
 	, syntax_description   = "`//` adds a single-line comment. `/*` and `*/` encapsulate a multi-line comment. Multi-line comments can be nested."
 	, syntax_doc_locations = [CLR 15 "B.2" "_Toc311798132"]
-	, syntax_examples      = []
+	, syntax_examples      = map EX
+		[ "Start = 37 // Single-line comment"
+		, "Start = /* inline or multi-line comment */ 37"
+		]
 	}
 
 bs_context =

backend/build.sh

 #!/bin/bash
 set -ev
 
-./install_clean.sh
+. ./install_clean_vars.sh
+install_clean.sh 'base lib-platform lib-tcpip'
 sed -i 's/cocl/cocl::-wmf/' /opt/clean/etc/IDEEnvs
 
 PACKAGES="patch jq unzip z3"

backend/install_clean.sh

-#!/bin/bash
-set -ev
-
-PATCHCLEANBUILD="sed -i 's:clean-compiler-and-rts compiler itask:cstaps compiler master:' clean-base/linux-x64/git-sources.txt; sed -i 's:compiler-itask:compiler-master:' clean-base/linux-x64/build.sh; sed -i 's:master:cloogle:' clean-lib-platform/linux-x64/git-sources.txt; sed -i 's:platform-master:platform-cloogle:' clean-lib-platform/linux-x64/build.sh" install_clean.sh 'base lib-dynamics lib-platform lib-tcpip' 2019-01-27

backend/install_clean_vars.sh

+#!/bin/bash
+
+PATCHCLEANBUILD="sed -i 's:clean-compiler-and-rts compiler itask:cstaps compiler cloogle:' clean-base/linux-x64/git-sources.txt"
+PATCHCLEANBUILD="$PATCHCLEANBUILD;sed -i 's:compiler-itask:compiler-cloogle:' clean-base/linux-x64/build.sh"
+PATCHCLEANBUILD="$PATCHCLEANBUILD;sed -i 's:master:cloogle:' clean-lib-platform/linux-x64/git-sources.txt"
+PATCHCLEANBUILD="$PATCHCLEANBUILD;sed -i 's:platform-master:platform-cloogle:' clean-lib-platform/linux-x64/build.sh"
+export PATCHCLEANBUILD
+
+export CLEANDATE="2019-01-30"

test/builtin_syntax.icl → backend/test/builtin_syntax.icl

@@ -6,7 +6,6 @@ import StdMaybe
 import Clean.Types
 import Clean.Types.Parse
 from Data.Func import mapSt, seqSt
-import Data.List
 import System.CommandLine
 import System.Directory
 import System.File
@@ -52,9 +51,6 @@ Start w
 
 test :: !SyntaxEntry !*(!Int, !Int, !*World) -> *(!Int, !Int, !*World)
 test se (i,failed,w)
-# (comments_ok,i,w) = check_style se (i,w)
-# failed = failed + if comments_ok 0 1
-
 # err = stderr <<< "Checking syntax for '" <<< se.syntax_title <<< "': "
 # (_,w) = fclose err w
 # (results,(j,w)) = mapSt test_example se.syntax_examples (i,w)
@@ -67,59 +63,6 @@ test se (i,failed,w)
 
 = (j,failed + length [f \\ f=:False <- results],w)
 
-check_style :: !SyntaxEntry !*(!Int, !*World) -> *(!Bool, !Int, !*World)
-check_style se (i,w)
-# err = stderr
-# err = if comment_alignment_ok
-	err
-	(err
-		<<< "\033[0;31mComment alignment is inconsistent for '"
-		<<< se.syntax_title
-		<<< "' (at most two different levels may be used):\033[0m\n\t"
-		<<< join "\n\t" example_lines
-		<<< "\n")
-# err = case no_spaces_around_comments of
-	[] -> err
-	ns -> err
-		<<< "\033[0;31mThese lines in '"
-		<<< se.syntax_title
-		<<< "' contain comments without spaces around the '//':\033[0m\n\t"
-		<<< join "\n\t" ns
-		<<< "\n"
-# err = case missing_spaces of
-	[] -> err
-	ns -> err
-		<<< "\033[0;31mThese lines in '"
-		<<< se.syntax_title
-		<<< "' contain list comprehension elements without spaces around them:\033[0m\n\t"
-		<<< join "\n\t" ns
-		<<< "\n"
-# (_,w) = fclose err w
-= (True,i+1,w)
-where
-	example_lines = concatMap (split "\n") [replaceSubString "\t" "    " e.example \\ e <- se.syntax_examples]
-
-	comment_alignment_ok = length (removeDup comments) < 3
-	where
-		comments = filter ((<>) -1) [indexOf "//" l \\ l <- example_lines]
-
-	no_spaces_around_comments = filter bad example_lines
-	where
-		bad s = case indexOf "//" s of
-			-1 -> False
-			i  -> s.[i-1] <> ' ' || s.[i+2] <> ' '
-
-	missing_spaces = filter bad example_lines
-	where
-		bad s
-		# s = replaceSubString "'\\\\'" "" s // special case for '\\' in basic_values
-		# (results,_) = mapSt check ["<|-","<-:","<-","\\\\"] s
-		= or results
-
-		check op s
-		# new = replaceSubString (" " +++ op +++ " ") "" s
-		= (indexOf op new >= 0, new)
-
 test_example :: !SyntaxExample !*(!Int, !*World) -> *(!Bool, !*(!Int, !*World))
 test_example {example,cleanjs_start,bootstrap,requires_itask_compiler} (i,w)
 | requires_itask_compiler

test/Makefile

-CLM:=clm
-CLMFLAGS:=-nr -nt\
-	-I ../backend\
-	-I ../backend/Cloogle\
-	-I ../backend/Cloogle/libcloogle\
-	-I ../backend/Cloogle/CleanRegex\
-	-IL Platform
-
-BIN:=builtin_syntax
-TEST:=$(addprefix test_,$(BIN))
-
-test: $(TEST)
-
-$(TEST): test_%: %
-	./$<
-
-$(BIN): .FORCE
-	$(CLM) $(CLMFLAGS) $@ -o $@
-
-.FORCE:
-
-.PHONY: test .FORCE