Skip to content
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.

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

Fix CI #518

Merged
merged 11 commits into from
Sep 20, 2022
Merged
Changes from all commits
Commits
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
22 changes: 13 additions & 9 deletions .github/workflows/build_docker.yml
Original file line number Diff line number Diff line change
@@ -3,12 +3,7 @@ name: Build with ocp Docker container
# The goal of this workflow is to test the installation of the project with opam
# on a specific light docker container instead of using default GH-actions one.

on:
push:
branches:
- fix-ci
- next
- main
on: [push,pull_request]

jobs:
install_docker:
@@ -20,16 +15,25 @@ jobs:
# as a system compiler. This container also contains opam 2.1.
container:
image: ocamlpro/ocaml:4.10
options: --user root

steps:
# This line is needed to acces and use opam. We are unable to set the user
# to `ocaml` with the container parameters
- run: sudo chmod a+wx .

# Checkout the code of the current branch
- name: Checkout code
uses: actions/checkout@v2

# Switch to ocaml user
- run: su ocaml

# This line is needed to acces and use opam. We are unable to set the user
# to `ocaml` with the container parameters
- run: sudo chmod a+wx .

# This line is needed to allow the working directory to be used even
# the ocaml user do not have rights on it.
- run: git config --global --add safe.directory /__w/alt-ergo/alt-ergo

# Create a switch with the system compiler (no compilation needed).
# And then, install external (no need for depext with opam 2.1) and libs deps.
- run: opam switch create . ocaml-system --deps-only
9 changes: 2 additions & 7 deletions .github/workflows/build_macos.yml
Original file line number Diff line number Diff line change
@@ -3,12 +3,7 @@ name: Build MacOS
# This workflow try to build and test Alt-Ergo on a MacOS system
# If the build succed, an artifact with the alt-ergo binary is uploaded
# It only runs on `next` or `main` branch
on:
push:
branches:
- fix-ci
- next
- main
on: [push,pull_request]

env:
OCAML_DEFAULT_VERSION: 4.10.0
@@ -63,7 +58,7 @@ jobs:

# Install dependencies
- name: Install deps
run: opam install ./*.opam --deps-only --with-test --depext
run: opam install ./*.opam --deps-only --with-test


# Build and install with opam
2 changes: 1 addition & 1 deletion .github/workflows/linter.yml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
name: Linter

on: push
on: [push,pull_request]

env:
OCAML_DEFAULT_VERSION: 4.10.0
6 changes: 3 additions & 3 deletions src/bin/gui/annoted_ast.ml
Original file line number Diff line number Diff line change
@@ -40,7 +40,7 @@ let font = GPango.font_description_from_string font_str
let font_size = font#size

let make_indent nb =
String.make (min max_indent (nb * indent_size)) ' '
String.make (min max_indent (nb * indent_size)) ' '

type sbuffer = GSourceView3.source_buffer

@@ -234,12 +234,12 @@ let set_font ?(family=font#family) ?(size=font#size) ?(ratio=1.) () =
font#modify ~family:family ~size:new_sz ();
Gui_config.update_font_family font#family;
Gui_config.update_font_size font#size

let update_font envs =
List.iter (fun env ->
env.goal_view#misc#modify_font font;
env.inst_view#misc#modify_font font) envs

let increase_size envs =
set_font ~ratio:1.1 ();
(* Printer.print_dbg "Increase font size: %d" font#size; *)
30 changes: 22 additions & 8 deletions src/bin/gui/connected_ast.ml
Original file line number Diff line number Diff line change
@@ -693,8 +693,12 @@ and axiom_callback t env ~origin:y z i =
let menu = GMenu.menu () in
let menu_item = GMenu.menu_item ~packing:menu#append () in
let vbox = GPack.hbox ~packing:menu_item#add () in
let _ = GMisc.label ~text:"Instanciate axiom ..." ~packing:vbox#add () in
let _ = GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add () in
let _ =
GMisc.label ~text:"Instanciate axiom ..." ~packing:vbox#add ()
in
let _ =
GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add ()
in
ignore(menu_item#connect#activate
~callback:(popup_axiom t env offset));
menu#popup ~button:3 ~time:(GdkEvent.Button.time z);
@@ -784,7 +788,7 @@ and popup_trigger t qid env (sbuf:sbuffer) offset () =
~packing:pop_w#vbox#add ()
in
let tv1 = GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
~show_line_numbers:true ~wrap_mode:`CHAR()
~show_line_numbers:true ~wrap_mode:`CHAR()
in
let _ = tv1#misc#modify_font font in
let _ = tv1#set_editable true in
@@ -822,8 +826,12 @@ and triggers_callback t qid env sbuf ~origin:y z i =
let menu = GMenu.menu () in
let menu_item = GMenu.menu_item ~packing:menu#append () in
let vbox = GPack.hbox ~packing:menu_item#add () in
let _ = GMisc.label ~text:"Add trigger(s) ..." ~packing:vbox#add () in
let _ = GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add () in
let _ =
GMisc.label ~text:"Add trigger(s) ..." ~packing:vbox#add ()
in
let _ =
GMisc.image ~stock:`ADD ~icon_size:`MENU ~packing:vbox#add ()
in
ignore(menu_item#connect#activate
~callback:(popup_trigger t qid env sbuf offset));
menu#popup ~button:3 ~time:(GdkEvent.Button.time z);
@@ -971,15 +979,21 @@ let show_used_lemmas env expl =
clear_used_lemmas_tags env;
let max_mul = MTag.fold (fun _ m acc -> max acc m) ftags 0 in
let green_0 =
Gdk.Color.color_parse (Gui_util.dec_to_hex_color (65535*3/4) 65535 (65535*3/4))
Gdk.Color.color_parse (
Gui_util.dec_to_hex_color (65535*3/4) 65535 (65535*3/4)
)
in
List.iter (fun t -> t#set_property (`BACKGROUND_GDK green_0)) atags;
MTag.iter (fun t m ->
let perc = ((max_mul - m) * 65535) / max_mul in
let green_n = Gdk.Color.color_parse
(Gui_util.dec_to_hex_color (perc*1/2) ((perc + 2*65535) /3) (perc*1/2)) in
(Gui_util.dec_to_hex_color
(perc*1/2)
((perc + 2*65535) /3) (perc*1/2)
)
in
t#set_property (`BACKGROUND_GDK green_n)) ftags;
env.proof_tags <- ftags;
env.proof_tags <- ftags;
env.proof_toptags <- atags


2 changes: 1 addition & 1 deletion src/bin/gui/gui_config.ml
Original file line number Diff line number Diff line change
@@ -94,7 +94,7 @@ let write () =
let update_window_size width height =
window_width := width;
window_height := height

let update_font_family family =
font_family := family

5 changes: 3 additions & 2 deletions src/bin/gui/gui_util.mli
Original file line number Diff line number Diff line change
@@ -26,8 +26,9 @@
(* License version 2.0 *)
(* *)
(******************************************************************************)

(** Convert RGB color given in the decimal format (red, green, blue) where
red, green and blue are integers between 0 and 65535
to RGB color in hexadecimal format #rrrrggggbbbb where r, g, b are hexadecimal digits. *)
to RGB color in hexadecimal format #rrrrggggbbbb where r, g, b are
hexadecimal digits. *)
val dec_to_hex_color : int -> int -> int -> string
57 changes: 38 additions & 19 deletions src/bin/gui/main_gui.ml
Original file line number Diff line number Diff line change
@@ -232,7 +232,7 @@ let pop_model sat_env () =
~packing:pop_w#vbox#add () in
let buf1 = GSourceView3.source_buffer () in
let tv1 = GSourceView3.source_view ~source_buffer:buf1 ~packing:(sw1#add)
~wrap_mode:`CHAR () in
~wrap_mode:`CHAR () in
let _ = tv1#misc#modify_font font in
let _ = tv1#set_editable false in
let model_text = asprintf "%a@." (SAT.print_model ~header:false) sat_env in
@@ -953,7 +953,7 @@ let search_one buf str result (iter:GText.iter ref) found_all_tag =
result := !iter#forward_search str;
match !result with
| None -> ()
| Some (i1, i2) ->
| Some (i1, i2) ->
buf#apply_tag found_all_tag ~start:i1 ~stop:i2;
iter := i2

@@ -1085,7 +1085,7 @@ let start_gui all_used_context =
let toolbox = GPack.hbox ~border_width:0 ~packing:rbox#pack () in

let toolbar = GButton.toolbar (*~tooltips:true*)
~packing:toolbox#add ~style: `BOTH () in
~packing:toolbox#add ~style: `BOTH () in
toolbar#set_icon_size `DIALOG;

let hb = GPack.paned `HORIZONTAL
@@ -1165,15 +1165,21 @@ let start_gui all_used_context =
st_ctx annoted_ast dep actions resulting_ids in
connect env;

let remove_ctx_button = GButton.toggle_tool_button ~label:" Remove context"
~stock:`CUT ~packing:toolbar#insert () in
ignore(remove_ctx_button#connect#clicked ~callback:(remove_context env));

let remove_ctx_button =
GButton.toggle_tool_button ~label:" Remove context"
~stock:`CUT ~packing:toolbar#insert ()
in
ignore (
remove_ctx_button#connect#clicked ~callback:(remove_context env)
);

let run_button = GButton.tool_button ~label:" Run Alt-Ergo"
~stock:`EXECUTE () in
~stock:`EXECUTE () in
toolbar#insert run_button;

let stop_button = GButton.tool_button ~label:" Abort" ~stock:`STOP () in
let stop_button =
GButton.tool_button ~label:" Abort" ~stock:`STOP ()
in
stop_button#misc#hide ();

(* TODO: Use toolbar#insert instead of insert_space *)
@@ -1188,24 +1194,35 @@ let start_gui all_used_context =

ignore(toolbar#insert tool_item);

let clean_button = GButton.tool_button ~label:" Clean unused" ~stock:`CLEAR () in
let clean_button =
GButton.tool_button ~label:" Clean unused" ~stock:`CLEAR ()
in
toolbar#insert clean_button;
clean_button#misc#hide ();

let toolsearch =
GButton.toolbar (*~tooltips:true*) ~packing:(toolbox#pack ~fill:true) ()
GButton.toolbar
(*~tooltips:true*)
~packing:(toolbox#pack ~fill:true)
()
in
toolsearch#set_icon_size `DIALOG;

let tool_item = GButton.tool_item ~packing:toolsearch#insert () in
let search_box = GPack.hbox ~spacing:5 ~border_width:5 ~packing:tool_item#add () in
let search_box =
GPack.hbox ~spacing:5 ~border_width:5 ~packing:tool_item#add ()
in
ignore(GMisc.image ~icon_size:`LARGE_TOOLBAR
~stock:`FIND ~packing:search_box#add ());
let search_entry = GEdit.entry ~packing:search_box#add () in

let search_forw_button = GButton.tool_button ~stock:`GO_DOWN ~packing:toolsearch#insert () in
let search_back_button = GButton.tool_button ~stock:`GO_UP ~packing:toolsearch#insert () in

let search_forw_button =
GButton.tool_button ~stock:`GO_DOWN ~packing:toolsearch#insert ()
in
let search_back_button =
GButton.tool_button ~stock:`GO_UP ~packing:toolsearch#insert ()
in

let found_all_tag = buf1#create_tag [`BACKGROUND "yellow"] in
let found_tag = buf1#create_tag [`BACKGROUND "orange"] in

@@ -1258,8 +1275,10 @@ let start_gui all_used_context =

ignore(run_button#connect#clicked
~callback:(
run run_button stop_button clean_button inst_model timers_model
result_image result_label thread env used_context));
run
run_button stop_button clean_button inst_model
timers_model result_image result_label thread env
used_context));

ignore(stop_button#connect#clicked
~callback:(kill_thread thread));
@@ -1311,7 +1330,7 @@ let start_gui all_used_context =
)) envs
in

(* The GtkFontChooserDialog is not yet implemented by lablgtk3. *)
(* The GtkFontChooserDialog is not yet implemented by lablgtk3. *)
(*let choose_font () =
let font_win = GWindow.font_selection_dialog
~parent:w
@@ -1390,7 +1409,7 @@ let start_gui all_used_context =
(* `M ("Options", options_entries); *)
(* `M ("Help", help_entries) *)
(* ] in *)

let create_menu label menubar =
let item = GMenu.menu_item ~label ~packing:menubar#append () in
GMenu.menu ~packing:item#set_submenu ()