Skip to content

fix parsing of bare open: do not load modules as require open does #1450

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

Merged
fblanqui merged 2 commits into from
Jul 9, 2026
+13 −6
Merged

fix parsing of bare open: do not load modules as require open does #1450

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4d9e95d
parser: map a bare open to P_open again
ciaran-matthew-dunne Jul 9, 2026
1a9657b
revert CHANGES because the problem was not in the previous release
fblanqui Jul 9, 2026
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 src/parsing/lpParser.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,11 +433,15 @@ let term_id (lb:'token lexbuf): p_term =

(* commands *)

let open_ (priv:bool) (lb:'token lexbuf) : p_command_aux =
(* [req] tells whether the command starts with the [require] keyword:
[require [private] open] loads the modules and opens them
([P_require]), while a bare [[private] open] only opens modules
that are already loaded ([P_open]). *)
let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux =
if log_enabled() then log "%s" __FUNCTION__;
consume OPEN lb;
let ps = nelist path_tks path lb in
P_require(Some priv,ps)
if req then P_require(Some priv,ps) else P_open(priv,ps)

let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux =
if log_enabled() then log "%s" __FUNCTION__;
Expand Down Expand Up @@ -520,7 +524,7 @@ and command (lb:'token lexbuf) : p_command =
end
| [{elt=P_expo Term.Privat;_}] ->
begin match current_token lb with
| OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb)
| OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ false true lb)
| SYMBOL ->
extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb)
| L_PAREN
Expand All @@ -546,10 +550,10 @@ and command (lb:'token lexbuf) : p_command =
begin
match current_token lb with
| OPEN ->
extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb)
extend_pos lb (*__FUNCTION__*) pos1 (open_ true false lb)
| PRIVATE ->
consume_token lb;
extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb)
extend_pos lb (*__FUNCTION__*) pos1 (open_ true true lb)
| QID _ ->
let ps = nelist path_tks path lb in
begin
Expand All @@ -570,7 +574,7 @@ and command (lb:'token lexbuf) : p_command =
| _ -> expected lb "" [OPEN;PRIVATE;QID[]]
end
| OPEN ->
extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb)
extend_pos lb (*__FUNCTION__*) pos1 (open_ false false lb)
| SYMBOL ->
extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb)
| L_PAREN
Expand Down
3 changes: 3 additions & 0 deletions tests/KO/open_not_required.lp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
// A bare [open] does not load modules: the module must have been
// required first (with [require] or [require open]).
open tests.OK.boolean;
Loading