Support native compilation of HOL Light, add unit tests #87

	name: CI

	on:
	# Allows you to run this workflow manually from the Actions tab
	workflow_dispatch:

	# check PRs
	pull_request:
	branches:
	- master

	# check pushes
	push:
	branches:
	- master

	jobs:
	test1:
	runs-on: ubuntu-22.04
	name: OCaml 4.05, Camlp5 7.10

	steps:
	- name: Install dependency
	run: \|
	sudo apt update && sudo apt install -y opam
	opam init --disable-sandboxing --compiler=4.05.0
	opam pin -y add camlp5 7.10
	opam install -y num ledit

	- name: Checkout this repo
	uses: actions/checkout@v2
	with:
	path: hol-light

	- name: Run
	run: \|
	cd hol-light
	eval $(opam env)
	make
	./hol.sh 2>&1 \| tee log.txt
	! grep "Error" log.txt
	grep "Camlp5 parsing version (HOL-Light)" log.txt

	test2:
	runs-on: ubuntu-22.04
	name: OCaml 4.14, Camlp5 8.03 (make switch)

	steps:
	- name: Install dependency
	run: \|
	sudo apt update && sudo apt install -y opam xdot
	opam init --disable-sandboxing

	- name: Checkout this repo
	uses: actions/checkout@v2
	with:
	path: hol-light

	- name: Run
	run: \|
	cd hol-light
	make switch
	eval $(opam env)
	make
	./hol.sh 2>&1 \| tee log.txt
	! grep "Error" log.txt
	grep "Camlp5 parsing version (HOL-Light)" log.txt
	cd ..

	- name: Run (HOLLIGHT_USE_MODULE=1)
	run: \|
	cd hol-light
	eval $(opam env)
	make clean
	export HOLLIGHT_USE_MODULE=1
	make
	./hol.sh \| tee log.txt
	! grep "Error" log.txt
	grep "Camlp5 parsing version (HOL-Light)" log.txt
	./unit_tests.byte
	./unit_tests.native

Provide feedback