Add windows CI

.github/workflows/build.yml

@@ -6,7 +6,7 @@ name: ci
 
 jobs:
   build:
-    name: Build
+    name: Build Linux
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v2
@@ -17,3 +17,42 @@ jobs:
       - name: test
         working-directory: tests
         run: env METAMATH=../metamath ./run_test.sh *.in
+
+  build-win-msvc:
+    name: Build Windows (MSVC)
+    runs-on: windows-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: ilammy/msvc-dev-cmd@v1
+
+      - name: build
+        working-directory: src
+        run: cl.exe *.c
+
+      - name: run
+        working-directory: src
+        run: ./metamath.exe
+
+      - name: test
+        working-directory: tests
+        shell: bash
+        run: env METAMATH=../src/metamath.exe ./run_test.sh *.in
+
+  build-win-gcc:
+    name: Build Windows (GCC)
+    runs-on: windows-latest
+    steps:
+      - uses: actions/checkout@v2
+
+      - name: build
+        working-directory: src
+        run: gcc *.c -o metamath.exe
+
+      - name: run
+        working-directory: src
+        run: ./metamath.exe
+
+      - name: test
+        working-directory: tests
+        shell: bash
+        run: env METAMATH=../src/metamath.exe ./run_test.sh *.in

src/metamath.c

@@ -725,7 +725,7 @@ void command(int argc, char *argv[]);
  * \param argc int number of commandline parameters
  * \param argv (char*)[] array of \a argc commandline parameters, followed by NULL
  * \return success 0 else failure
- * 
+ *
  * Running metamath
  *   ./metamath 'read set.mm' 'verify proof *'
  * will start main with \a argc set to 2, argv[0] to "read set.mm", argv[1]
@@ -752,6 +752,9 @@ int main(int argc, char *argv[]) {
 
   g_toolsMode = g_listMode;
 
+  printf("sizeof(long) = %ld\n", sizeof(long));
+  printf("len(null) = %ld\n", pntrLen(NULL_PNTRSTRING));
+
   if (!g_listMode) {
     /*print2("Metamath - Version %s\n", MVERSION);*/
     print2("Metamath - Version %s%s", MVERSION, space(27 - (long)strlen(MVERSION)));

src/mmdata.c

@@ -2410,20 +2410,21 @@ temp_pntrString *pntrCat(const pntrString *string1,...) {
 
 }
 
+#define pntrPoolLoc(s) (size_t)((s)[-3])
+#define pntrAllocSize(s) (size_t)((s)[-2])
+#define pntrActualSize(s) (size_t)((s)[-1])
 
 
 /* Find out the length of a pntrString */
 long pntrLen(const pntrString *s) {
   /* Assume it's been allocated with poolMalloc. */
-  return ((((const long *)s)[-1] - (long)(sizeof(pntrString)))
-      / (long)(sizeof(pntrString)));
+  return (pntrActualSize(s) - sizeof(pntrString)) / sizeof(pntrString);
 }
 
 
 /* Find out the allocated length of a pntrString */
 long pntrAllocLen(const pntrString *s) {
-  return ((((long *)s)[-2] - (long)(sizeof(pntrString)))
-    / (long)(sizeof(pntrString)));
+  return (pntrAllocSize(s) - sizeof(pntrString)) / sizeof(pntrString);
 }
 
 /* Set the actual size field in a pntrString allocated with poolFixedMalloc() */
@@ -2435,12 +2436,12 @@ long pntrAllocLen(const pntrString *s) {
 /* ???Note that pntrZapLen's not moving string to used pool wastes potential
    space when called by the routines in this module.  Effect should be minor. */
 void pntrZapLen(pntrString *s, long length) {
-  if (((long *)s)[-3] != -1) {
+  if (pntrPoolLoc(s) != (size_t)-1) {
     /* It's already in the used pool, so adjust free space tally */
-    poolTotalFree = poolTotalFree + ((long *)s)[-1]
+    poolTotalFree = poolTotalFree + (long)pntrActualSize(s)
         - (length + 1) * (long)(sizeof(pntrString));
   }
-  ((long *)s)[-1] = (length + 1) * (long)(sizeof(pntrString));
+  ((size_t *)s)[-1] = (size_t)(length + 1) * sizeof(pntrString);
 /*E*/if(db9)getPoolStats(&i1,&j1_,&k1); if(db9)printf("l: pool %ld stat %ld\n",poolTotalFree,i1+j1_);
 }
 

src/mmdata.h

@@ -21,7 +21,7 @@
  */
 typedef char flag;
 
-/*! 
+/*!
  * \var flag g_listMode.
  * Obsolete.  Now fixed to 0.  Historically the metamath sources were also used
  * for other purposes than maintaining Metamath files.  One such application, a
@@ -261,10 +261,10 @@ extern struct nullNmbrStruct g_NmbrNull;
  * describing a block of memory of pntrString containing only the
  * null pointer.  Besides the pointer it is accompanied with a header matching
  * the hidden administrative values of a usual pntrString managed as a stack.
- * 
+ *
  * The values in this administrative header are such that it is never subject to
  * memory allocation or deallocation.
- * 
+ *
  * \bug The C standard does not require a long having the same size as a
  * void*.  In fact there might be **no** integer type matching a pointer in size.
  */
@@ -274,28 +274,28 @@ struct nullPntrStruct {
      * An instance of a nullPntrStruct is always standalone and never part of a
      * larger pool.  Indicated by the fixed value -1.
      */
-    long poolLoc;
-    /*! 
+    size_t poolLoc;
+    /*!
      * allocated size of the memory block containing the \a pntrString.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
-     * single void* instance. 
+     * single void* instance.
      */
-    long allocSize;
-    /*! 
+    size_t allocSize;
+    /*!
      * currently used size of the memory block containing the \a pntrString.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
      * single pointer element.
      */
-    long actualSize;
-    /*! 
+    size_t actualSize;
+    /*!
      * memory for a single void* instance, set and fixed to the null pointer.
      */
     pntrString nullElement; };
 /*!
  * \var g_PntrNull. Global instance of a memory block structured like a
  * \a pntrString, but fixed in size and containing always exactly one null
  * pointer element.
- * 
+ *
  * \attention mark as const
  */
 extern struct nullPntrStruct g_PntrNull;
@@ -498,7 +498,7 @@ temp_pntrString *pntrPSpace(long n);
 /*!
  * \fn long pntrLen(const pntrString* s) Determine the length of a pntrString
  * \param s \a pntrString array of pointers from its hidden structure.
- * \pre s has a hidden structure, see \a pntrString 
+ * \pre s has a hidden structure, see \a pntrString
  */
 long pntrLen(const pntrString *s);
 long pntrAllocLen(const pntrString *s);

src/mmpars.c

@@ -162,8 +162,8 @@ char *readRawSource(vstring fileBuf, long *size) {
 
   if (fbPtr != fileBuf + charCount) {
     /* To help debugging: */
-    printf("fbPtr=%ld fileBuf=%ld charCount=%ld diff=%ld\n",
-        (long)fbPtr, (long)fileBuf, charCount, fbPtr - fileBuf - charCount);
+    printf("fbPtr=%p fileBuf=%p charCount=%ld diff=%ld\n",
+        (void*)fbPtr, (void*)fileBuf, charCount, (long)(fbPtr - fileBuf) - charCount);
     bug(1704);
   }