Commit 0cd2eeb9 authored by Simon Vandevelde's avatar Simon Vandevelde
Browse files

Merge branch 'web144' into 'main'

move `web-IDP-Z3` folder into `IDP-Z3/idp_web_client` folder

Closes #144

See merge request !203
parents a5c44824 32da44c0
Pipeline #457431422 passed with stages
in 6 minutes and 3 seconds
idp_web_client/dist
idp_web_client/node_modules
monkeytype.sqlite3
bin
lib64
......
......@@ -13,8 +13,8 @@ Contributors (alphabetical): Bram Aerts, Ingmar Dasseville, Jo Devriendt, Marc
* Install [python3](https://www.python.org/downloads/) on your machine.
* Install [poetry](https://python-poetry.org/docs/#installation):
* after that, logout and login if requested, to update `$PATH`
* Use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine
* Open a terminal in that directory
* Use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine, e.g., IDP-Z3
* Open a terminal in that IDP-Z3 directory
* If you have several versions of python3, and want to run on a particular one, e.g., 3.9:
* run `poetry env use 3.9`
* replace `python3` by `python3.9` in every command below
......@@ -28,11 +28,30 @@ To launch the Interactive Consultant web server:
* open a terminal in that directory and run `poetry run python3 main.py`
* open your browser at http://127.0.0.1:5000
The Web IDE is at http://127.0.0.1:5000/IDE
# Develop
You may want to read about the [technical documentation](http://docs.idp-z3.be/en/latest/code_reference.html) and the [Development and deployment guide](https://gitlab.com/krr/IDP-Z3/-/wikis/Development-and-deployment-guide).
Development on the web client requires additional installation:
* install [nvm](https://github.com/nvm-sh/nvm)
* `cd idp_web_client`
* `nvm install 11`
* `npm ci`
To launch the Interactive Consultant in development mode:
* open a terminal in the IDP-Z3 directory and run `poetry run python3 main.py` to launch the IDP-Z3 server
* `cd idp_web_client`
* `npm start`
* open your browser at http://127.0.0.1:4201
# documentation
The user manual is in the `/docs` folder and can be locally generated as follows:
~~~~
poetry run sphinx-autobuild docs docs/_build/html
......
......@@ -49,17 +49,17 @@ run('python3 test.py generate')
update_statics = query_user("Update the '/IDP-Z3/idp_server/static' folder? (Y/n) ")
if update_statics:
require_clean_work_tree("../web-IDP-Z3")
require_clean_work_tree("idp_web_client")
# Generate static and commit.
run('npm run-script build', cwd='../web-IDP-Z3', check=True)
run('npm run-script build', cwd='idp_web_client', check=True)
print("Copying to static folder ...")
copy_tree('../web-IDP-Z3/dist/', './idp_server/static')
copy_tree('idp_web_client/dist/', './idp_server/static')
# Check if web-IDP-Z3 is on latest version and clean.
branch = get('git rev-parse --abbrev-ref HEAD', cwd="../web-IDP-Z3")
assert branch == b'main\n', \
"Cannot deploy: web-IDP-Z3 not in main branch !"
# branch = get('git rev-parse --abbrev-ref HEAD', cwd="idp_web_client")
# assert branch == b'main\n', \
# "Cannot deploy: web-IDP-Z3 not in main branch !"
# Verify we are on main branch.
branch = get('git rev-parse --abbrev-ref HEAD')
......@@ -104,10 +104,11 @@ if update_statics:
if new_tag:
# create tag in both projects
run(f"git tag {tag_version}")
run(f"git -C ../web-IDP-Z3 tag {tag_version}")
# run(f"git -C idp_web_client tag {tag_version}")
# Push tags.
run(f"git push origin {tag_version}")
run(f"git -C ../web-IDP-Z3 push origin {tag_version}")
# run(f"git -C idp_web_client push origin {tag_version}")
# Publish new version on Pypi.
run("poetry install")
......@@ -123,7 +124,7 @@ if update_statics:
# Push to google repository and deploy on GAE.
run("git push google main")
run("git push google main", cwd='../web-IDP-Z3')
run("git push google main", cwd='idp_web_client')
run(f"gcloud app deploy {'' if new_tag else '--no-promote'}")
# update versions.list at https://gist.github.com/IDP-Z3/5d82c61fa39e8aa23da1642a2e2b420a
......
......@@ -8,12 +8,12 @@ Essentially, the IDP-Z3 components translate the requested inferences on the kno
## Web clients
The repository for the web clients is in a [separate GitLab repository](https://gitlab.com/krr/web-IDP-Z3).
The source code for the web clients is in the [IDP_Z3_web_client folder](https://gitlab.com/krr/IDP-Z3/-/tree/main/idp_web_client).
The clients are written in [Typescript](https://www.typescriptlang.org/), using the [Angular](https://angular.io/) framework (version 7.1), and the [primeNG](https://www.primefaces.org/primeng/#/) library of widgets. 
It uses the [Monaco editor](https://www.npmjs.com/package/ngx-monaco-editor).
The interactions with the server are controlled by [idp.service.ts](https://gitlab.com/krr/web-IDP-Z3/blob/main/src/services/idp.service.ts)
The [AppSettings file](https://gitlab.com/krr/web-IDP-Z3/blob/main/src/services/AppSettings.ts) contains important settings, such as the address of the IDP-Z3 sample theories.
The interactions with the server are controlled by [idp.service.ts](https://gitlab.com/krr/IDP-Z3/blob/main/idp_web_client/src/services/idp.service.ts)
The [AppSettings file](https://gitlab.com/krr/IDP-Z3/blob/main/idp_web_client/src/services/AppSettings.ts) contains important settings, such as the address of the IDP-Z3 sample theories.
The web clients are sent to the browser by the IDP-Z3 server as static files.
The static files are generated by the `/IDP-Z3/deploy.py` script as part of the deployment, and saved in the `/IDP-Z3/idp_server/static` folder.
......@@ -130,7 +130,7 @@ The graph of calls is outlined in `/docs/zettlr/Call graph.md`.
The code is organised by steps, not by classes: for example, all methods to annotate an expression by another are grouped in [Annotate.py](/code_modules/engine_annotate). We use [monkey-patching](https://www.geeksforgeeks.org/monkey-patching-in-python-dynamic-behavior/) to attach methods to the classes declared in another module.
Important classes of the IDP-Z3 engine are: [Expression](/code_modules/engine_expression#idp_engine.Expression.Expression), [Assignment](/code_modules/engine_assignments#idp_engine.Assignments.Assignment), [Theory](/code_modules/engine_problem#idp_engine.Problem.Theory).
Important classes of the IDP-Z3 engine are: [Expression](/code_modules/engine_expression#idp_engine.Expression.Expression), [Assignment](/code_modules/engine_assignments#idp_engine.Assignments.Assignment), [Theory](/code_modules/engine_problem#idp_engine.Theory.Theory).
Substitute() modifies the AST "in place". Because the results of step 1-2 are cached, steps 4-7 are done after copying the AST (custom `copy()`).
......
......@@ -55,7 +55,7 @@ Many operations on Theory instances can be chained, e.g., ``Theory(T,S).propagat
The class has the following methods:
.. autoclass:: idp_engine.Problem.Theory
.. autoclass:: idp_engine.Theory.Theory
:members:
.. _idp_engine:
......
.. _solver_problem:
idp_engine.Problem
idp_engine.Theory
=========================
.. automodule:: idp_engine.Problem
.. automodule:: idp_engine.Theory
:members:
:noindex:
......@@ -13,10 +13,10 @@ Steps to push on heroku:
Steps to release an anonymized version of the code:
* delete autconfigz3/bin, /lib, /lib64, _pycache_
* in web-IDP-Z3/src/app/app.component.html
* in IDP-Z3/idp_web_client/src/app/app.component.html
* remove KUL logo
* remove footerContainer with Flemish Impuls program
* in web-IDP-Z3/src/app/header/header.component.ts
* in IDP-Z3/idp_web_client/src/app/header/header.component.ts
* remove Help / Tutorial entry
* link for reference: `AppSettings.ORIGIN+'/docs/_build/html/index.html'`
* in IDP-Z3/README.md: adapt as necessary
......
......@@ -36,7 +36,7 @@ X IC: do not restart propagation if model is unknown: it won't fix anything
- [x] API propagate: consider all assignments without value
- [x] API problem: fill assignments with all subtences
X API: restart solver if unknown (not needed ?)
- [ ] move definitions, constraints, assignments to State.Problem just before get_relevant
- [ ] move definitions, constraints, assignments to State.Theory just before get_relevant
- [X] API: add simplify
- [X] IC: do not cascade propagate: full propagate will take care of it. Use API.simplify instead
- [ ] API: add tag argument to propagate
......
......@@ -19,15 +19,14 @@
"""
Methods to interpret a theory in a data structure
Methods to ground / interpret a theory in a data structure
* substitute a constant by its value in an expression
* replace symbols interpreted in a structure by their interpretation
* expand quantifiers
* replace symbols interpreted in the structure by their interpretation
This module also includes methods to:
* substitute an node by another in an AST tree
* substitute a node by another in an AST tree
* instantiate an expresion, i.e. replace a variable by a value
This module monkey-patches the ASTNode class and sub-classes.
......
......@@ -38,7 +38,7 @@ from .Expression import (Expression, AQuantification,
ADisjunction, AConjunction, AppliedSymbol,
AComparison, AUnary, Brackets, TRUE, FALSE)
from .Parse import str_to_IDP
from .Problem import Theory
from .Theory import Theory
from .utils import OrderedSet, IDPZ3Error, NOT_SATISFIABLE
start = time.process_time()
......
......@@ -22,7 +22,7 @@ This module contains the logic for the computation of relevance.
from idp_engine.Assignments import Status as S
from idp_engine.Expression import (AppliedSymbol, TRUE, Expression, AQuantification,
AConjunction, Brackets, UnappliedSymbol)
from idp_engine.Problem import Theory
from idp_engine.Theory import Theory
from idp_engine.utils import OrderedSet, GOAL_SYMBOL, RELEVANT
......
......@@ -28,7 +28,7 @@ from typing import Any, Iterator, List, Union
from z3 import Solver
from .Parse import IDP, TheoryBlock, Structure
from .Problem import Theory
from .Theory import Theory
from .Assignments import Status as S, Assignments
from .utils import NEWL
......
......@@ -6,7 +6,7 @@ from .Simplify import Done
from .Idp_to_Z3 import Done
from .Run import (model_check, model_expand, model_propagate,
execute, decision_table)
from .Problem import Propagation, Theory
from .Theory import Propagation, Theory
from .Propagate import Done
from .Relevance import Done
from .Assignments import Status, Assignment, Assignments
# Editor configuration, see https://editorconfig.org
root = true
[*]
charset = utf-8
indent_style = space
indent_size = 2
insert_final_newline = true
trim_trailing_whitespace = true
[*.md]
max_line_length = off
trim_trailing_whitespace = false
{
"$schema": "./node_modules/@angular/cli/lib/config/schema.json",
"version": 1,
"newProjectRoot": "projects",
"projects": {
"web-IDP-Z3": {
"root": "",
"sourceRoot": "src",
"projectType": "application",
"prefix": "app",
"schematics": {},
"architect": {
"build": {
"builder": "@angular-devkit/build-angular:browser",
"options": {
"outputPath": "dist/",
"index": "src/index.html",
"main": "src/main.ts",
"polyfills": "src/polyfills.ts",
"tsConfig": "src/tsconfig.app.json",
"assets": [
"src/favicon.ico",
"src/assets",
{ "glob": "**/*", "input": "node_modules/ngx-monaco-editor/assets/", "output": "./assets/" }
],
"styles": [
"node_modules/primeng-lts/resources/themes/nova-light/theme.css",
"node_modules/primeng-lts/resources/primeng.min.css",
"node_modules/primeicons/primeicons.css",
"src/styles.css"
],
"scripts": [
"node_modules/isotope-layout/dist/isotope.pkgd.min.js",
"node_modules/isotope-packery/packery-mode.pkgd.min.js"
]
},
"configurations": {
"production": {
"fileReplacements": [
{
"replace": "src/environments/environment.ts",
"with": "src/environments/environment.prod.ts"
}
],
"optimization": true,
"outputHashing": "all",
"sourceMap": false,
"extractCss": true,
"namedChunks": false,
"aot": true,
"extractLicenses": true,
"vendorChunk": false,
"buildOptimizer": true,
"budgets": [
{
"type": "initial",
"maximumWarning": "2mb",
"maximumError": "5mb"
}
]
}
}
},
"serve": {
"builder": "@angular-devkit/build-angular:dev-server",
"options": {
"browserTarget": "web-IDP-Z3:build"
},
"configurations": {
"production": {
"browserTarget": "web-IDP-Z3:build:production"
}
}
},
"extract-i18n": {
"builder": "@angular-devkit/build-angular:extract-i18n",
"options": {
"browserTarget": "web-IDP-Z3:build"
}
},
"test": {
"builder": "@angular-devkit/build-angular:karma",
"options": {
"main": "src/test.ts",
"polyfills": "src/polyfills.ts",
"tsConfig": "src/tsconfig.spec.json",
"karmaConfig": "src/karma.conf.js",
"styles": [
"src/styles.css"
],
"scripts": [],
"assets": [
"src/favicon.ico",
"src/assets"
]
}
},
"lint": {
"builder": "@angular-devkit/build-angular:tslint",
"options": {
"tsConfig": [
"src/tsconfig.app.json",
"src/tsconfig.spec.json"
],
"exclude": [
"**/node_modules/**"
]
}
}
}
},
"web-IDP-Z3-e2e": {
"root": "e2e/",
"projectType": "application",
"prefix": "",
"architect": {
"e2e": {
"builder": "@angular-devkit/build-angular:protractor",
"options": {
"protractorConfig": "e2e/protractor.conf.js",
"devServerTarget": "web-IDP-Z3:serve"
},
"configurations": {
"production": {
"devServerTarget": "web-IDP-Z3:serve:production"
}
}
},
"lint": {
"builder": "@angular-devkit/build-angular:tslint",
"options": {
"tsConfig": "e2e/tsconfig.e2e.json",
"exclude": [
"**/node_modules/**"
]
}
}
}
}
},
"defaultProject": "web-IDP-Z3"
}
// Protractor configuration file, see link for more information
// https://github.com/angular/protractor/blob/master/lib/config.ts
const { SpecReporter } = require('jasmine-spec-reporter');
exports.config = {
allScriptsTimeout: 11000,
specs: [
'./src/**/*.e2e-spec.ts'
],
capabilities: {
'browserName': 'chrome'
},
directConnect: true,
baseUrl: 'http://localhost:4200/',
framework: 'jasmine',
jasmineNodeOpts: {
showColors: true,
defaultTimeoutInterval: 30000,
print: function() {}
},
onPrepare() {
require('ts-node').register({
project: require('path').join(__dirname, './tsconfig.e2e.json')
});
jasmine.getEnv().addReporter(new SpecReporter({ spec: { displayStacktrace: true } }));
}
};
\ No newline at end of file
import { AppPage } from './app.po';
describe('workspace-project App', () => {
let page: AppPage;
beforeEach(() => {
page = new AppPage();
});
it('should display welcome message', () => {
page.navigateTo();
expect(page.getTitleText()).toEqual('Welcome to the Interactive Consultant!');
});
});
import { browser, by, element } from 'protractor';
export class AppPage {
navigateTo() {
return browser.get('/');
}
getTitleText() {
return element(by.css('app-root h1')).getText();
}
}
{
"extends": "../tsconfig.json",
"compilerOptions": {
"outDir": "../out-tsc/app",
"module": "commonjs",
"target": "es5",
"types": [
"jasmine",
"jasminewd2",
"node"
]
}
}
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment