Skip to content

Be more resilient to garbage arguments passed to rocq check. #21910

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ppedrot wants to merge 1 commit into
base: master
Choose a base branch
from
+10 −6
Open

Be more resilient to garbage arguments passed to rocq check. #21910

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 10 additions & 6 deletions checker/coqchk_main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,10 @@ let dirpath_of_string s =
| [] -> CheckLibrary.default_root_prefix
| dir -> DirPath.make (List.map Id.of_string dir)
let path_of_string s =
if Filename.check_suffix s ".vo" then CheckLibrary.PhysicalFile s
if Filename.check_suffix s ".vo" then Ok (CheckLibrary.PhysicalFile s)
else match parse_dir s with
| [] -> invalid_arg "path_of_string"
| l::dir -> CheckLibrary.LogicalFile {dirpath=dir; basename=l}
| [] -> Error ()
| l::dir -> Ok (CheckLibrary.LogicalFile {dirpath=dir; basename=l})

let get_version env () =
match env with
Expand Down Expand Up @@ -165,17 +165,21 @@ let make_senv () =
let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
Safe_typing.set_native_compiler false senv

let try_add_path s l = match path_of_string s with
| Ok path -> path :: l
| Error () -> CErrors.user_err (str "Invalid path " ++ qstring s)
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why not user_err directly in path_of_string?

Copy link
Copy Markdown
Member Author

@ppedrot ppedrot Apr 9, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I hesitated to put a warning rather than an error, and written that way it makes it easy to replace it locally.


let admit_list = ref ([] : CheckLibrary.object_file list)
let add_admit s =
admit_list := path_of_string s :: !admit_list
admit_list := try_add_path s !admit_list

let norec_list = ref ([] : CheckLibrary.object_file list)
let add_norec s =
norec_list := path_of_string s :: !norec_list
norec_list := try_add_path s !norec_list

let compile_list = ref ([] : CheckLibrary.object_file list)
let add_compile s =
compile_list := path_of_string s :: !compile_list
compile_list := try_add_path s !compile_list

(*s Parsing of the command line.
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
Expand Down
Loading