File: coqProject.ml

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2
file content (73 lines) | stat: -rw-r--r-- 2,024 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
open OUnit
open Utest
open CoqProject_file

let tests = ref []
let add_test name test = tests := (mk_test name (TestCase test)) :: !tests

let sourced_file x = { thing = x; source = ProjectFile }

(* Implicit argument for `read_project_file` *)
let warning_fn _ = ()

let t () =
  let project_file_contents = "" in
  bracket_tmpfile
  (fun (project_file_path, project_file_channel) ->
    output_string project_file_channel project_file_contents;
    flush project_file_channel;
    let expected : project = {
      project_file = Some project_file_path;
      makefile = None;
      native_compiler = None;
      docroot = None;

      v_files = [];
      ml_files = [];
      mli_files = [];
      mlg_files = [];
      mllib_files = [];
      mlpack_files = [];
      meta_file = Absent;

      ml_includes = [];
      r_includes = [];
      q_includes = [];
      extra_args = [];
      defs = [];
    } in
    assert_equal expected (read_project_file ~warning_fn project_file_path)
  ) ()
let _ = add_test "empty file" t

let t () =
  let project_file_contents = "-arg \"-w default\" -arg -w -arg foo -arg \"-set 'Default Goal Selector=!'\"" in
  bracket_tmpfile
  (fun (project_file_path, project_file_channel) ->
    output_string project_file_channel project_file_contents;
    flush project_file_channel;
    let expected : project = {
      project_file = Some project_file_path;
      makefile = None;
      native_compiler = None;
      docroot = None;

      v_files = [];
      ml_files = [];
      mli_files = [];
      mlg_files = [];
      mllib_files = [];
      mlpack_files = [];
      meta_file = Absent;

      ml_includes = [];
      r_includes = [];
      q_includes = [];
      extra_args = List.map sourced_file ["-w"; "default"; "-w"; "foo"; "-set"; "Default Goal Selector=!"];
      defs = [];
    } in
    assert_equal expected (read_project_file ~warning_fn project_file_path)
  ) ()
let _ = add_test "-arg separation" t

let _ = run_tests __FILE__ (open_log_out_ch __FILE__) (List.rev !tests)