Merge branch 'feature/dune/ivette' into 'feature/bobot/jbuilder'

Ivette build in Dune branch

See merge request frama-c/frama-c!3775

.gitlab-ci.yml

@@ -55,19 +55,19 @@ header-check:
   tags:
     - nix
 
-# ivette:
-#   stage: build
-#   image: node:lts-gallium
-#   cache:
-#     paths:
-#       - ivette/node_modules/
-#   script:
-#     - node --version
-#     - npm --version
-#     - yarn --version
-#     - make -C ivette
-#   tags:
-#     - docker
+ivette:
+  stage: build
+  image: node:lts-gallium
+  cache:
+    paths:
+      - ivette/node_modules/
+  script:
+    - node --version
+    - npm --version
+    - yarn --version
+    - make -C ivette
+  tags:
+    - docker
 
 lint:
   stage: build

ivette/Makefile

@@ -106,15 +106,11 @@ update-distrib-files:
 
 api:
 	@echo "[Ivette] Generating TypeScript API"
-	@find src/frama-c -path "*/api/*" -name "*.ts" -exec rm -f {} \;
-	../bin/frama-c.byte \
-		-load-module src/frama-c/api_generator.ml \
-		-server-tsc
-	@find src/frama-c -path "*/api/*" -name "*.ts" \
-		-exec headache \
-			-h ../headers/open-source/CEA_LGPL \
-			-c ../headers/headache_config.txt {} \;\
-		-exec chmod a-w {} \;
+	./api.sh build src
+
+check-api:
+	@echo "[Ivette] Checking TypeScript API"
+	./api.sh check src
 
 # --------------------------------------------------------------------------
 # --- Ivette Documentation

ivette/api.sh

+#!/bin/bash
+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2022                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+if [[ $# != 2 ]];
+then
+  cat <<EOF
+usage: $0 [check|build] path
+EOF
+  exit 2
+fi
+
+case "$1" in
+  "build") ;;
+  "check") ;;
+  *)
+    echo "Bad first parameter: $1"
+    echo "Exiting without doing anything.";
+    exit 31
+esac
+action="$1"
+
+if [[ ! -d $2 ]]; then
+  echo "$2 directory doesn't exist"
+fi
+path=$2
+
+build () {
+  build_path=$1
+
+  find $build_path/frama-c -path "*/api/*" -name "*.ts" -exec rm -f {} \;
+	../bin/frama-c -server-tsc -server-tsc-out $build_path
+	find $build_path/frama-c -path "*/api/*" -name "*.ts" \
+		-exec headache \
+			-h ../headers/open-source/CEA_LGPL \
+			-c ../headers/headache_config.txt {} \;\
+		-exec chmod a-w {} \;
+}
+
+tmp=
+cleanup () {
+  if [[ -n $tmp ]]; then
+    rm -rf $tmp
+  fi
+}
+
+check () {
+  check_path=$1
+  tmp="$(mktemp -d)"
+  trap cleanup EXIT
+
+  cp -r $check_path/frama-c $tmp/frama-c
+  build $tmp
+  diff -r $check_path/frama-c $tmp/frama-c
+}
+
+case "$action" in
+  "build") build $path ;;
+  "check") check $path ;;
+esac

ivette/src/frama-c/kernel/api/services/index.ts

@@ -64,15 +64,14 @@ import { tag } from 'frama-c/kernel/api/data';
 
 const getConfig_internal: Server.GetRequest<
   null,
-  { pluginpath: string[], libdir: string, datadir: string, version: string }
+  { pluginpath: string[], datadir: string[], version: string }
   > = {
   kind: Server.RqKind.GET,
   name:   'kernel.services.getConfig',
   input:  Json.jNull,
   output: Json.jObject({
             pluginpath: Json.jList(Json.jString),
-            libdir: Json.jFail(Json.jString,'String expected'),
-            datadir: Json.jFail(Json.jString,'String expected'),
+            datadir: Json.jList(Json.jString),
             version: Json.jFail(Json.jString,'String expected'),
           }),
   signals: [],
@@ -80,7 +79,7 @@ const getConfig_internal: Server.GetRequest<
 /** Frama-C Kernel configuration */
 export const getConfig: Server.GetRequest<
   null,
-  { pluginpath: string[], libdir: string, datadir: string, version: string }
+  { pluginpath: string[], datadir: string[], version: string }
   >= getConfig_internal;
 
 const load_internal: Server.SetRequest<string,string | undefined> = {

nix/pkgs.nix

@@ -32,6 +32,7 @@ let
     full-tests = oself.callPackage ./full-tests.nix {};
     kernel-tests = oself.callPackage ./kernel-tests.nix {};
     plugins-tests = oself.callPackage ./plugins-tests.nix {};
+    ts-api = oself.callPackage ./ts-api.nix {};
     wp-tests = oself.callPackage ./wp-tests.nix {};
 
     # Internal tests

nix/ts-api.nix

+{ lib
+, stdenv
+, frama-c
+, headache
+} :
+
+stdenv.mkDerivation rec {
+  pname = "ts-api-check";
+  version = frama-c.version;
+  slang = frama-c.slang;
+
+  src = frama-c.build_dir + "/dir.tar";
+  sourceRoot = ".";
+
+  buildInputs = frama-c.buildInputs ++ [
+    frama-c
+    headache
+  ];
+
+  postPatch = ''
+    patchShebangs .
+  '' ;
+  preConfigure = frama-c.preConfigure;
+
+  # Keep main configuration
+  configurePhase = ''
+    true
+  '';
+
+  buildPhase = ''
+    make -C ivette check-api
+  '';
+
+  # No installation required
+  installPhase = ''
+    touch $out
+  '';
+}

ivette/src/frama-c/api_generator.ml → src/plugins/api-generator/api_generator.ml

@@ -559,20 +559,22 @@ let makePackage pkg path fmt =
 (* -------------------------------------------------------------------------- *)
 
 let generate () =
-  begin
-    Pkg.iter
-      begin fun pkg ->
-        let path = pkg_path ~plugin:pkg.p_plugin ~package:pkg.p_package in
-        Self.feedback "Package %s" path ;
-        let out = OUT.get () in
-        let file = Printf.sprintf "%s/%s/index.ts" out path in
-        let dir = Filename.dirname file in
-        if not (Sys.file_exists dir && Sys.is_directory dir) then
-          Extlib.mkdir ~parents:true dir 0o755 ;
-        Command.print_file file (makePackage pkg path) ;
-      end
-  end
-
-let () = Db.Main.extend generate
+  if TSC.get () then
+    begin
+      Pkg.iter
+        begin fun pkg ->
+          let path = pkg_path ~plugin:pkg.p_plugin ~package:pkg.p_package in
+          Self.feedback "Package %s" path ;
+          let out = OUT.get () in
+          let file = Printf.sprintf "%s/%s/index.ts" out path in
+          let dir = Filename.dirname file in
+          if not (Sys.file_exists dir && Sys.is_directory dir) then
+            Extlib.mkdir ~parents:true dir 0o755 ;
+          Command.print_file file (makePackage pkg path) ;
+        end
+    end
+
+let () =
+  Db.Main.extend generate
 
 (* -------------------------------------------------------------------------- *)

src/plugins/api-generator/dune

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of Frama-C.                                         ;;
+;;                                                                        ;;
+;;  Copyright (C) 2007-2022                                               ;;
+;;    CEA (Commissariat à l'énergie atomique et aux énergies              ;;
+;;         alternatives)                                                  ;;
+;;                                                                        ;;
+;;  you can redistribute it and/or modify it under the terms of the GNU   ;;
+;;  Lesser General Public License as published by the Free Software       ;;
+;;  Foundation, version 2.1.                                              ;;
+;;                                                                        ;;
+;;  It is distributed in the hope that it will be useful,                 ;;
+;;  but WITHOUT ANY WARRANTY; without even the implied warranty of        ;;
+;;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         ;;
+;;  GNU Lesser General Public License for more details.                   ;;
+;;                                                                        ;;
+;;  See the GNU Lesser General Public License version 2.1                 ;;
+;;  for more details (enclosed in the file licenses/LGPLv2.1).            ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+( library
+  (name api_generator)
+  (public_name frama-c-api-generator.core)
+  (flags -open Frama_c_kernel :standard -w -9)
+  (libraries frama-c.kernel frama-c-server.core)
+)
+
+(plugin (optional) (name api_generator) (libraries frama-c-api-generator.core) (site (frama-c plugins)))

src/plugins/api-generator/dune-project

+(lang dune 2.8)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;                                                                        ;;
+;;  This file is part of Frama-C.                                         ;;
+;;                                                                        ;;
+;;  Copyright (C) 2007-2022                                               ;;
+;;    CEA (Commissariat à l'énergie atomique et aux énergies              ;;
+;;         alternatives)                                                  ;;
+;;                                                                        ;;
+;;  you can redistribute it and/or modify it under the terms of the GNU   ;;
+;;  Lesser General Public License as published by the Free Software       ;;
+;;  Foundation, version 2.1.                                              ;;
+;;                                                                        ;;
+;;  It is distributed in the hope that it will be useful,                 ;;
+;;  but WITHOUT ANY WARRANTY; without even the implied warranty of        ;;
+;;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         ;;
+;;  GNU Lesser General Public License for more details.                   ;;
+;;                                                                        ;;
+;;  See the GNU Lesser General Public License version 2.1                 ;;
+;;  for more details (enclosed in the file licenses/LGPLv2.1).            ;;
+;;                                                                        ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(name frama-c-api-generator)
+(using dune_site 0.1)