MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 94b1bdd4 authored by Stefan Berghofer's avatar Stefan Berghofer
Browse files

Merge

parents 82407c0e 5e51326c
......@@ -270,6 +270,7 @@ Scheduled for 31 october 2013
* Patch de johannes pour les noms de fichier pour Isabelle TODO
* discriminate, mettre les bons arguments par defaut (ANDREI)
DONE ?
* eliminate_match: (apres la release ?)
** faire un cas particulier pour "bool", le match pouvant se traduire
......
......@@ -133,13 +133,32 @@ let (why_lang, any_lang) =
| Some _ as l -> l in
(why_lang, any_lang)
(* Borrowed from Frama-C src/gui/source_manager.ml:
Try to convert a source file either as UTF-8 or as locale. *)
let try_convert s =
try
if Glib.Utf8.validate s then s else Glib.Convert.locale_to_utf8 s
with Glib.Convert.Error _ ->
try
Glib.Convert.convert_with_fallback
~fallback:"#neither UTF-8 nor locale nor ISO-8859-15#"
~to_codeset:"UTF-8"
~from_codeset:"ISO_8859-15"
s
with Glib.Convert.Error _ as e -> Printexc.to_string e
let source_text fname =
let ic = open_in fname in
let size = in_channel_length ic in
let buf = String.create size in
really_input ic buf 0 size;
close_in ic;
buf
try
let ic = open_in fname in
let size = in_channel_length ic in
let buf = String.create size in
really_input ic buf 0 size;
close_in ic;
try_convert buf
with e when not (Debug.test_flag Debug.stack_trace) ->
"Error while opening or reading file '" ^ fname ^ "':\n" ^ (Printexc.to_string e)
(********************************)
(* loading WhyIDE configuration *)
......
......@@ -981,13 +981,18 @@ let print_task printer_args realize ?old fmt task =
| _ -> assert false
) Mid.empty task in
(* 2 cases: goal is clone T with [] or goal is a real goal *)
let realized_theories =
match task with
| None -> assert false
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, _) }}} ->
realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
Mid.remove th.Theory.th_name realized_theories
| _ -> realized_theories in
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
Mid.remove th.Theory.th_name realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
Task.task_prev = task } ->
upd_realized_theories task
| _ -> assert false in
let realized_theories = upd_realized_theories task in
let realized_theories' =
Mid.map (fun (th,s) -> fprintf fmt "Require %s.@\n" s; th) realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in
......
......@@ -17,7 +17,6 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Printer
let ident_printer =
......
......@@ -833,21 +833,21 @@ let print_task printer_args realize ?old fmt task =
| _ -> assert false
) Mid.empty task in
(* two cases: task is clone T with [] or task is a real goal *)
let thname, thpath, realized_theories = match task with
| None -> assert false
let rec upd_realized_theories = function
| Some { Task.task_decl = { Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
id_unique thprinter pr.pr_name, [], realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Clone (th,_) }} ->
Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
let id = th.Theory.th_name in
id_unique thprinter id,
th.Theory.th_path, Mid.remove id realized_theories
| Some { Task.task_decl = { Theory.td_node = td } } ->
let name = match td with
| Theory.Decl { Decl.d_node = Dprop (_, pr, _) } ->
id_unique thprinter pr.pr_name
| _ -> "goal"
in
name, [], realized_theories
in
let id = th.Theory.th_name in
id_unique thprinter id,
th.Theory.th_path,
Mid.remove id realized_theories
| Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
Task.task_prev = task } ->
upd_realized_theories task
| _ -> assert false in
let thname, thpath, realized_theories = upd_realized_theories task in
(* make names as stable as possible by first printing all identifiers *)
let realized_theories' = Mid.map fst realized_theories in
let realized_symbols = Task.used_symbols realized_theories' in
......
......@@ -17,7 +17,6 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Printer
(** SMTLIB tokens taken from CVC4: src/parser/smt2/Smt2.g *)
......
......@@ -17,7 +17,6 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Printer
let ident_printer =
......
......@@ -2103,7 +2103,7 @@ let rec recompute_all_shapes_goal ~release g =
g.goal_checksum <- Termcode.task_checksum t;
if release then release_task g;
iter_goal
(fun pa -> ())
(fun _pa -> ())
(iter_transf (recompute_all_shapes_goal ~release))
(iter_metas (recompute_all_shapes_goal ~release))
g
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment