Admin/Linux/Isabelle.c
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 54314 8f7061babae4
child 71338 373dcdd363dc
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
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>
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    11
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
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
    14
{
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    15
  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
    16
  exit(2);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    17
}
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
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
    21
{
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    22
  char **cmd_line = NULL;
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    23
  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
    24
54314
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    25
  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
    26
  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
    27
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    28
  cmd_line[0] = malloc(strlen(argv[0]) + 5);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    29
  if (cmd_line[0] == 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
    30
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    31
  strcpy(cmd_line[0], argv[0]);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    32
  strcat(cmd_line[0], ".run");
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    33
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    34
  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
    35
54314
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    36
  cmd_line[argc] = NULL;
8f7061babae4 proper NULL termination;
wenzelm
parents: 54313
diff changeset
    37
54313
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    38
  execvp(cmd_line[0], cmd_line);
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    39
  fail("Failed to execute application script");
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    40
}
da2e6282a4f5 native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
wenzelm
parents:
diff changeset
    41