/seL4-l4v-master/HOL4/developers/docfiles/ |
H A D | gen-documented.sh | 14 ls -1 $holdir/help/Docfiles/*.doc | sed 's/.*s\/\([^/]\+\)\.doc/\1/'
|
/seL4-l4v-master/HOL4/tools/ |
H A D | buildcline.sml | 15 fun from build_theory_graph debug help jobcount kernelspec multithread 20 help = help, 27 fun from' seqname selftest relocbuild multithread kernelspec jobcount help 32 help = help, 39 fun to f {build_theory_graph, debug, help, jobcount, kernelspec, multithread, 42 f build_theory_graph debug help jobcount kernelspec multithread relocbuild 116 {help = "build with experimental kernel", long = ["expk"], short = "", 118 {help [all...] |
H A D | buildcline_dtype.sml | 6 help : bool, 15 { kernelspec = NONE, jobcount = NONE, seqname = NONE, help = false,
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Help.sig | 2 (* Help -- on-line help functions *) 4 val help : string -> unit value 15 [help s] provides on-line help on the topic indicated by string s. 17 help "lib"; gives an overview of the Moscow ML library. 18 help "id"; provides help on identifier id (case-insensitive). 36 /str cyclically search for string str in help file (case-insensitive) 43 searched for help files. The directories are searched in order, 46 [indexfiles] is a reference to a list of full paths of help ter [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sml | 9 fun from debug do_logging fast help hmakefile holdir includes 17 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 33 hmakefile help fast do_logging debug = 36 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 46 fun to f {debug, do_logging, fast, help, hmakefile, holdir, 52 f debug do_logging fast help hmakefile holdir includes 71 help : bool, 97 help [all...] |
/seL4-l4v-master/l4v/misc/scripts/ |
H A D | gen_isabelle_root.py | 20 help="output file", metavar="FILE") 22 help="input directory", action="append", default=[], 25 help="isabelle session name", metavar="NAME") 27 help="isabelle base session", metavar="NAME") 29 help="additional named session dependency", action="append", default=[], 32 help="ROOT file should compile with \"quick and dirty\" enabled.", variable 36 help="Generate a theory file instead of a ROOT file.") variable 38 help="additional session directory", action="append",
|
H A D | thydeps | 106 help='Directories containing ROOT or ROOTS files (default: .)') 108 help='Show theory files from these directories (default: all)') 110 help='Path to Isabelle system') 112 help='Print relative paths to -b directory (only one dir allowed)') 114 help='Isabelle session names')
|
/seL4-l4v-master/seL4/tools/ |
H A D | hardware_gen.py | 42 group.add_argument('--' + name, help=task.__doc__.strip(), action='store_true') 67 parser.add_argument('--dtb', help='device tree blob to parse for generation', 69 parser.add_argument('--hardware-config', help='YAML file containing configuration for kernel devices', 71 parser.add_argument('--hardware-schema', help='YAML file containing schema for hardware config', 73 parser.add_argument('--arch', help='architecture to generate for', default='arm') 75 help='maximum address that is available as device untyped', type=int, default=32) 77 parser.add_argument('--enable-profiling', help='enable profiling',
|
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 151 help='Is this being generated for libsel4?') 154 help='Is this being generated for the arch layer?') 156 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-master/seL4/libsel4/tools/ |
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 151 help='Is this being generated for libsel4?') 154 help='Is this being generated for the arch layer?') 156 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 151 help='Is this being generated for libsel4?') 154 help='Is this being generated for the arch layer?') 156 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-master/HOL4/src/num/arith/Manual/ |
H A D | Makefile | 6 # Pathname to the arith help files 8 Help=../help 13 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-master/HOL4/src/num/reduce/Manual/ |
H A D | Makefile | 5 Help=../help 6 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-master/l4v/ |
H A D | run_tests | 73 help='test multiple L4V_ARCHs (comma-separated)') 76 help='test all L4V_ARCHes') 77 parser.add_argument('-h', '--help', action='store_true', 78 help=argparse.SUPPRESS) 93 if args.help: 95 print('Now printing help for main regression script:') 97 passthrough_args += ['--help']
|
/seL4-l4v-master/l4v/spec/cspec/ |
H A D | mk_umm_types.py | 38 help="C file to parse") 40 help="output filename") 42 help="add Isabelle ROOT or ROOTS file path", action='append')
|
/seL4-l4v-master/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 6 fun from chattiness files_wmatches help tests = 8 chattiness = chattiness, files_wmatches = files_wmatches, help = help, 11 fun from' tests help files_wmatches chattiness = 13 chattiness = chattiness, files_wmatches = files_wmatches, help = help, 16 fun to f {chattiness, files_wmatches, help, tests} = 17 f chattiness files_wmatches help tests 35 help : bool, 239 { help [all...] |
/seL4-l4v-master/seL4/tools/hardware/outputs/ |
H A D | compat_strings.py | 30 help='output file for compat strings list', type=argparse.FileType('w'))
|
/seL4-l4v-master/HOL4/src/coretypes/pair-Manual/ |
H A D | Makefile | 6 # Pathname to the string help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src/Doc2Tex.exe
|
/seL4-l4v-master/HOL4/src/res_quan/Manual/ |
H A D | Makefile | 6 # Pathname to the help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-master/HOL4/src/string/Manual/ |
H A D | Makefile | 6 # Pathname to the string help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src/Doc2Tex.exe
|
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | Makefile | 6 # Pathname to the unwind help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-master/HOL4/tools/Holmake/mosml/ |
H A D | HM_Cline.sml | 61 {help = "specify Moscow ML's base directory", long = ["mosmldir"], 77 (map (fn {desc,help,short,long} => 78 {desc = mapd desc, help = help, long = long, short = short})
|
/seL4-l4v-master/HOL4/tools/trailing-wspace/ |
H A D | trailingwspace.sml | 156 datatype cline_record = CR of { quiet : bool, action : action, help : bool} 157 val init = CR {quiet = false, action = Fix, help = false} 158 fun quiet_upd b (CR {action, help, ...}) = 159 CR {action = action, quiet = b, help = help} 160 fun act_upd a (CR {quiet, help, ...}) = 161 CR {action = a, quiet = quiet, help = help} 163 CR {action = action, quiet = quiet, help = b} 167 {short = "h", long = ["help"], des [all...] |
/seL4-l4v-master/HOL4/polyml/ |
H A D | missing | 28 echo 1>&2 "Try '$0 --help' for more information" 45 -h|--h|--he|--hel|--help) 53 -h, --help display this help and exit 74 echo 1>&2 "Try '$0 --help' for more information" 89 case $2 in --version|--help) exit $st;; esac
|
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_pseudoTools.sml | 17 (* Simple ML functions to help find good parameters for the linear
|