Searched refs:check (Results 1 - 25 of 420) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A DMakefile3 top: pkg-check.txt
11 pkg-check.txt: PKGS.lsp PKGS.sml
20 @echo "(note-chk-known-package-alist-success \"pkg-check.txt\" state)" >> $(TMPFILE)
22 @$(ACL2) < $(TMPFILE) > pkg-check.out 2> pkg-check.err
23 @if [ ! -e pkg-check.txt ]; then \
24 echo "FAILURE for pkg-check.txt" ; \
38 rm -f pkg-check.*
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala14 check: Set[String],
21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
37 check: Set[String],
45 conflicts(keywords, check, arg._1, arg._2)
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala14 check: Set[String],
21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
37 check: Set[String],
45 conflicts(keywords, check, arg._1, arg._2)
/seL4-l4v-master/HOL4/polyml/basis/
H A DInt32.sml34 fun check i = function
43 val fromLarge = check o fromLarge
44 val fromInt = check o fromInt
46 val ~ = check o ~
47 val op * = check o op *
48 val op + = check o op +
49 val op - = check o op -
50 val op div = check o op div
51 val op mod = check o op mod
52 val quot = check
[all...]
/seL4-l4v-master/isabelle/src/Pure/System/
H A Dlinux.scala20 /* check system */
28 if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
42 val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
68 echo = true).check
71 progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
88 val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
111 " " + Bash.string(name)).check
121 """).check
129 Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
161 Isabelle_System.bash("pwgen " + length + " 1").check
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/System/
H A Dlinux.scala20 /* check system */
28 if (Isabelle_System.bash("id -u").check.out != "0") error("Not running as superuser (root)")
42 val lines = Isabelle_System.bash("lsb_release -a").check.out_lines
68 echo = true).check
71 progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
88 val result = Isabelle_System.bash("getent passwd " + Bash.string(name)).check
111 " " + Bash.string(name)).check
121 """).check
129 Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
161 Isabelle_System.bash("pwgen " + length + " 1").check
[all...]
/seL4-l4v-master/HOL4/src/parse/
H A Dbase_tokens.sml23 fun check p exnstring (s,loc) = let function
25 fun check ss = function
28 | SOME (c,ss) => if p c then check ss
31 check (full s)
34 val check_binary = check (fn c => c = #"0" orelse c = #"1")
36 val check_octal = check (fn c => #"0" <= c andalso c <= #"7")
38 val check_hex = check (fn c => (#"0" <= c andalso c <= #"9") orelse
44 val check_decimal = check Char.isDigit "Illegal numeral"
H A DPrecAnalysis.sml62 fun check_for_listreductions check rels =
72 check(l,s) = NONE
83 (case check(s, tk1) of
85 (case check(valOf left_opt, tk1) of
93 | SOME l => (case check(l,tk1) of
105 case check (valOf left_opt, tk1) of
107 (case check (s, tk1) of
122 (case check (l, tk1) of
135 case check (valOf left_opt, tk2) of
137 (case check(tk
[all...]
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dmercurial.scala41 hg.command("root").check
60 hg.command(cmd, args, repository = false).check
101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
104 hg.command("heads", opt_template(template), options).check.out_lines
107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
112 hg.command("paths", args = args, options = options).check.out_lines
115 hg.command("manifest", opt_rev(rev), options).check.out_lines
118 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
129 hg.command("pull", opt_rev(rev) + optional(remote), options).check
132 rev: String = "", clean: Boolean = false, check
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dmercurial.scala41 hg.command("root").check
60 hg.command(cmd, args, repository = false).check
101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
104 hg.command("heads", opt_template(template), options).check.out_lines
107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
112 hg.command("paths", args = args, options = options).check.out_lines
115 hg.command("manifest", opt_rev(rev), options).check.out_lines
118 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
129 hg.command("pull", opt_rev(rev) + optional(remote), options).check
132 rev: String = "", clean: Boolean = false, check
[all...]
/seL4-l4v-master/isabelle/src/Pure/Concurrent/
H A Dsynchronized.scala33 def check(x: A): Option[B] =
44 check(x) match {
51 check(state)
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/
H A Dsynchronized.scala33 def check(x: A): Option[B] =
44 check(x) match {
51 check(state)
/seL4-l4v-master/HOL4/src/simp/src/
H A Dselftest.sml30 fun infloop_protect msg check f x =
31 (tprint msg; require (check_result check) f x)
68 "Bounded rewrites branch, and bypass permutative loop check"
88 fun check (th1, th2) = function
93 "Bounded rewrites override mk_rewrites loop check"
94 check
105 fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z`` function
109 check
120 fun check th = not (aconv (rhs (concl th)) ``x:bool``) function
124 check
135 fun check th = aconv (rhs (concl th)) result function
146 fun check th = aconv (rhs (concl th)) result function
157 fun check th = aconv (rhs (concl th)) result function
171 fun check (sgs, vfn) = let function
190 fun check th = th |> concl |> rhs |> aconv F function
200 fun check th = th |> concl |> rhs |> aconv F function
[all...]
/seL4-l4v-master/HOL4/src/1/theory_tests/
H A Dgithub115bScript.sml5 (* this theory is in the test-case solely to force Holmake to check that the
/seL4-l4v-master/HOL4/src/datatype/theory_tests/
H A Dndatatype_ind0Script.sml32 fun check (tac, t) = (tac([], t) before ignore (save_thm( function
37 val _ = map check [
/seL4-l4v-master/HOL4/src/string/theorytesting/
H A Dinjected_strlit3Script.sml8 (* check that the string injections from the base theory really have been
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dbuild_cygwin.scala39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
57 Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
H A Dbuild_polyml.scala113 """, redirect = true, echo = true).check
119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines
131 bash(dir1, "./build " + platform_64, redirect = true, echo = true).check
158 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
164 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
200 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
203 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
H A Dother_isabelle.scala53 other_isabelle("components -a", redirect = true, echo = echo).check
56 other_isabelle("getenv -b " + Bash.string(name)).check.out
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dbuild_cygwin.scala39 Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
57 Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
H A Dbuild_polyml.scala113 """, redirect = true, echo = true).check
119 val lines = bash(root, ldd + " target/bin/poly").check.out_lines
131 bash(dir1, "./build " + platform_64, redirect = true, echo = true).check
158 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
164 Bash.string("@executable_path/" + Path.explode(file).file_name) + " poly").check
200 "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
203 Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
H A Dother_isabelle.scala53 other_isabelle("components -a", redirect = true, echo = echo).check
56 other_isabelle("getenv -b " + Bash.string(name)).check.out
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C205 bool check = false; local
226 check = true;
243 if (proof != NULL || check) S.proof = new Proof();
252 if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof);
284 if (compress) { // ...compress, and possibly check
288 if (check)
293 } else if (check) { // ...check
/seL4-l4v-master/HOL4/src/HolQbf/
H A DHolQbfLib.sml45 QbfCertificate.VALID _ => QbfCertificate.check t dict cert
60 QbfCertificate.check t dict cert
74 QbfCertificate.check t dict cert
91 val th = QbfCertificate.check t' dict cert
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DSHA1_ML.sig8 * always return an empty vector and cannot be used to check for the end

Completed in 69 milliseconds

1234567891011>>