Admin/Linux/Isabelle.c
author wenzelm
Sat, 28 Nov 2020 16:25:29 +0100
changeset 72759 bd5ee3148132
parent 71363 ce3409dfb18c
child 73189 541f8630aa25
permissions -rw-r--r--
more antiquotations (reverting 4df341249348);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     1
/*  Author:     Makarius
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     2
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     3
Main Isabelle application executable.
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     4
*/
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     5
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     6
#include <stdlib.h>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     7
#include <stdio.h>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     8
#include <string.h>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
     9
#include <sys/types.h>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    10
#include <unistd.h>
71338
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    11
#include <libgen.h>
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    12
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    13
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    14
static void fail(const char *msg)
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    15
{
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    16
  fprintf(stderr, "%s\n", msg);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    17
  exit(2);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    18
}
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    19
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    20
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    21
int main(int argc, char *argv[])
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    22
{
71363
ce3409dfb18c clarified script name;
wenzelm
parents: 71338
diff changeset
    23
  char **cmd_line = NULL, *cmd = NULL, *dcmd = NULL, *dname = NULL;
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    24
  int i = 0;
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    25
71363
ce3409dfb18c clarified script name;
wenzelm
parents: 71338
diff changeset
    26
  dcmd = strdup(argv[0]);
ce3409dfb18c clarified script name;
wenzelm
parents: 71338
diff changeset
    27
  dname = dirname(dcmd);
71338
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    28
54314
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    29
  cmd_line = malloc(sizeof(char *) * (argc + 1));
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    30
  if (cmd_line == NULL) fail("Failed to allocate command line");
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    31
71338
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    32
  cmd = cmd_line[0];
71363
ce3409dfb18c clarified script name;
wenzelm
parents: 71338
diff changeset
    33
  cmd = malloc(strlen(dname) + strlen("/lib/scripts/Isabelle_app") + 1);
71338
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    34
  if (cmd == NULL) fail("Failed to allocate command name");
71363
ce3409dfb18c clarified script name;
wenzelm
parents: 71338
diff changeset
    35
  sprintf(cmd, "%s/lib/scripts/Isabelle_app", dname);
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    36
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    37
  for (i = 1; i < argc; i++) cmd_line[i] = argv[i];
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    38
54314
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    39
  cmd_line[argc] = NULL;
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    40
71338
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    41
  execvp(cmd, cmd_line);
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    42
  fprintf(stderr, "Failed to execute application script \"%s\"\n", cmd);
373dcdd363dc updated linux_app-20191223: x86_64-linux;
wenzelm
parents: 54314
diff changeset
    43
  exit(2);
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    44
}