Quelle component_bash_process.scala Sprache: Scala

/*  Title:      Pure/Admin/component_bash_process.scala
    Author:     Makarius

Build bash_process component from C source.
*/

package isabelle

object Component_Bash_Process {
  /* resources */

  def home: Path = Path.explode("$ISABELLE_BASH_PROCESS_HOME")

  def remote_program(directory: Components.Directory): Path = {
    val platform = directory.ssh.isabelle_platform.ISABELLE_PLATFORM(apple = true)
    directory.path + Path.basic(platform) + Path.basic("bash_process")
  }

  /* build bash_process */

  def build_bash_process(
    progress: Progress = new Progress,
    target_dir: Path = Path.current,
  ): Unit = {
    Isabelle_System.require_command("cc")

    /* component */

    val component_date = Date.Format.alt_date(Date.now())
    val component_name = "bash_process-" + component_date
    val component_dir =
      Components.Directory(target_dir + Path.basic(component_name))
        .create(progress = progress)
        .write_platforms()

    /* platform */

    val platform_name = Isabelle_Platform.local.ISABELLE_PLATFORM(apple = true)
    val platform_dir =
      Isabelle_System.make_directory(component_dir.path + Path.basic(platform_name))

    /* source */

    val source_file = Path.explode("bash_process.c")
    File.write(component_dir.path + source_file,
"""/* Author: Makarius
    License:    Isabelle BSD-3

Bash process with separate process group id.
*/

#include <signal.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <sys/resource.h>
#include <sys/time.h>
#include <sys/types.h>
#include <sys/wait.h>
#include <time.h>
#include <unistd.h>

static void fail(const char *msg)
{
  fprintf(stderr, "%s\n", msg);
  fflush(stderr);
  exit(2);
}

static time_t now()
{
  struct timeval tv;
  if (gettimeofday(&tv, NULL) == 0) {
    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
  }
  else {
    return time(NULL) * 1000;
  }
}

int main(int argc, char *argv[])
{
  /* args */

  if (argc < 2) {
    fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
    fflush(stderr);
    exit(1);
  }
  char *timing_name = argv[1];

  /* potential fork */

  time_t time_start = now();

  if (strlen(timing_name) > 0 || setsid() == -1) {
    pid_t pid = fork();

    if (pid == -1) fail("Cannot set session id (failed to fork)");
    else if (pid != 0) {
      int status;

      // ingore SIGINT
      struct sigaction sa;
      memset(&sa, 0, sizeof(sa));
      sa.sa_handler = SIG_IGN;
      sigaction(SIGINT, &sa, 0);

      if (waitpid(pid, &status, 0) == -1) {
        fail("Cannot join forked process");
      }

      /* report timing */

      if (strlen(timing_name) > 0) {
        long long timing_elapsed = now() - time_start;

        struct rusage ru;
        getrusage(RUSAGE_CHILDREN, &ru);

        long long timing_cpu =
          ru.ru_utime.tv_sec * 1000 + ru.ru_utime.tv_usec / 1000 +
          ru.ru_stime.tv_sec * 1000 + ru.ru_stime.tv_usec / 1000;

        FILE *timing_file = fopen(timing_name, "w");
        if (timing_file == NULL) fail("Cannot open timing file");
        fprintf(timing_file, "%lld %lld", timing_elapsed, timing_cpu);
        fclose(timing_file);
      }

      if (WIFEXITED(status)) {
        exit(WEXITSTATUS(status));
      }
      else if (WIFSIGNALED(status)) {
        exit(128 + WTERMSIG(status));
      }
      else {
        fail("Unknown status of forked process");
      }
    }
    else if (setsid() == -1) fail("Cannot set session id (after fork)");
  }

  /* report pid */

  fprintf(stdout, "%d\n", getpid());
  fflush(stdout);

  /* shift command line */

  int i;
  for (i = 2; i < argc; i++) {
    argv[i - 2] = argv[i];
  }
  argv[argc - 2] = NULL;
  argv[argc - 1] = NULL;

  /* exec */

  execvp("bash", argv);
  fail("Cannot exec process");
}
""")

    /* build */

    progress.echo("Building bash_process for " + platform_name + " ...")
    progress.bash("cc ../bash_process.c -o bash_process", cwd = platform_dir).check

    /* settings */

    component_dir.write_settings("""
ISABELLE_BASH_PROCESS_HOME="$COMPONENT"
ISABELLE_BASH_PROCESS="$ISABELLE_BASH_PROCESS_HOME/${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}/bash_process"
""")

    /* README */

    File.write(component_dir.README,
"""The bash_process executable has been built like this:

  cc -Wall bash_process.c -o bash_process

        Makarius
        """ + Date.Format.date(Date.now()) + "\n")
}

  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("component_bash_process", "build bash_process component from C source",
      Scala_Project.here,
      { args =>
        var target_dir = Path.current

        val getopts = Getopts("""
Usage: isabelle component_bash_process [OPTIONS]

  Options are:
    -D DIR       target directory (default ".")

  Build prover component from official download.
""",
          "D:" -> (arg => target_dir = Path.explode(arg)))

        val more_args = getopts(args)
        if (more_args.nonEmpty) getopts.usage()

        val progress = new Console_Progress()

        build_bash_process(progress = progress, target_dir = target_dir)
      })
}

quality96%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.